[Pkg-ocaml-maint-commits] r2658 -
/trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/coq-doc-html.doc-base.rectutorial
smimram at users.alioth.debian.org
smimram at users.alioth.debian.org
Sat Apr 29 17:06:23 UTC 2006
Author: smimram
Date: Sat Apr 29 17:06:22 2006
New Revision: 2658
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/?sc=1&rev=2658
Log:
Fixing doc-base.
Modified:
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/coq-doc-html.doc-base.rectutorial
Modified: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/coq-doc-html.doc-base.rectutorial
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/coq-doc-html.doc-base.rectutorial?rev=2658&op=diff
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/coq-doc-html.doc-base.rectutorial (original)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/coq-doc-html.doc-base.rectutorial Sat Apr 29 17:06:22 2006
@@ -1,4 +1,4 @@
-Document: coq-tutorial
+Document: coq-rectutorial
Title: The Coq Proof Assistant -- A Tutorial on [Co-]Inductive types in Coq
Author: Eduardo Giménez and Pierre Castéran
Abstract: This document is an introduction to the définition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script.
More information about the Pkg-ocaml-maint-commits
mailing list