passage V8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8342 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 282 insertions, 245 deletions

diff --git a/doc/RefMan-coi.tex b/doc/RefMan-coi.tex
index 7de3e69fe..ef5907016 100755
--- a/doc/RefMan-coi.tex
+++ b/doc/RefMan-coi.tex
@@ -52,7 +52,8 @@ An example of a co-inductive type is the type of infinite sequences formed with
 elements of type $A$, or streams for shorter. In Coq, 
 it can be introduced using the \verb!CoInductive! command~:
 \begin{coq_example}
-CoInductive Set Stream [A:Set] := cons : A->(Stream A)->(Stream A).
+CoInductive Stream (A:Set) : Set :=
+    cons : A -> Stream A -> Stream A.
 \end{coq_example}
 
 The syntax of this command is the same as the 
@@ -70,8 +71,12 @@ and $\tl: (\Str\;A)\rightarrow (\Str\;A)$  :
 \begin{coq_example}
 Section Destructors.
 Variable A : Set.
-Definition hd  := [x:(Stream A)]Cases x of (cons a s) => a end.
-Definition tl  := [x:(Stream A)]Cases x of (cons a s) => s end.
+Definition hd (x:Stream A) := match x with
+                              | cons a s => a
+                              end.
+Definition tl (x:Stream A) := match x with
+                              | cons a s => s
+                              end.
 \end{coq_example}
 \begin{coq_example*}
 End Destructors.
@@ -147,9 +152,9 @@ introduce the definitions above, $\from$ and $\alter$ will be accepted,
 while $\zeros$ and $\filter$ will be rejected giving some explanation 
 about why.
 \begin{coq_example}
-CoFixpoint zeros : (Stream nat) := (cons nat O (tl nat zeros)).
-CoFixpoint zeros : (Stream nat) := (cons nat O zeros).
-CoFixpoint from  : nat->(Stream nat) := [n:nat](cons nat n (from (S n))).
+CoFixpoint zeros  : Stream nat := cons nat 0%N (tl nat zeros).
+CoFixpoint zeros  : Stream nat := cons nat 0%N zeros.
+CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)).
 \end{coq_example}
 
 As in the \verb!Fixpoint! command (cf. section~\ref{Fixpoint}), it is possible 
@@ -171,9 +176,9 @@ Isolately it is considered as a canonical expression which
 is completely evaluated. We can test this using the command \verb!Compute! 
 to calculate the normal forms of some terms~:
 \begin{coq_example}
-Eval Compute in (from O).
-Eval Compute in (hd nat (from O)).
-Eval Compute in (tl nat (from O)).  
+Eval compute in (from 0).
+Eval compute in (hd nat (from 0)).
+Eval compute in (tl nat (from 0)).
 \end{coq_example}
 \noindent Thus, the equality 
 $(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$
@@ -184,7 +189,9 @@ a general lemma stating that eliminating and then re-introducing a stream
 yields the same stream.
 \begin{coq_example}
 Lemma unfold_Stream :
-        (x:(Stream nat))(x=(Cases x of (cons a s) => (cons nat a s) end)).
+   forall x:Stream nat, x = match x with
+                            | cons a s => cons nat a s
+                            end.
 \end{coq_example}
  
 \noindent The proof is immediate from the analysis of 
@@ -192,11 +199,11 @@ the possible cases for $x$, which transforms
 the equality in a trivial one.
 
 \begin{coq_example}
-Destruct x.
-Trivial.
+olddestruct x.
+trivial.
 \end{coq_example}
 \begin{coq_eval}
-Save.
+Qed.
 \end{coq_eval}
 The application of this lemma to  $(\from\;n)$ puts this
 constant at the head of an application which is an  argument 
@@ -204,7 +211,7 @@ of a case analysis, forcing its expansion.
 We can test the type of this application using Coq's command \verb!Check!,
 which infers the type of a given term. 
 \begin{coq_example}
-Check [n:nat](unfold_Stream  (from n)).
+Check (fun n:nat => unfold_Stream (from n)).
 \end{coq_example}
  \noindent  Actually, The elimination of $(\from\;n)$ has actually 
 no effect, because it is followed by a re-introduction, 
@@ -214,7 +221,7 @@ desired proposition. We can test this computing
 the normal form of the application above to see its type.  
 \begin{coq_example}
 Transparent unfold_Stream.
-Eval Compute in [n:nat](unfold_Stream  (from n)).
+Eval compute in (fun n:nat => unfold_Stream (from n)).
 \end{coq_example}
 
 
@@ -229,9 +236,9 @@ of construction a finite number of times, which is not always
 enough. Consider for example the following method for appending 
 two streams~:
 \begin{coq_example}
-Variable A:Set.
-CoFixpoint conc :  (Stream A)->(Stream A)->(Stream A) 
-        := [s1,s2:(Stream A)](cons A (hd A s1) (conc (tl A s1) s2)).
+Variable A : Set.
+CoFixpoint conc (s1 s2:Stream A) : Stream A :=
+  cons A (hd A s1) (conc (tl A s1) s2).
 \end{coq_example}
 
 Informally speaking, we expect that for all pair of streams $s_1$ and $s_2$, 
@@ -258,10 +265,10 @@ heads of the streams, and an (infinite) proof of the equality
 of their tails. 
 
 \begin{coq_example}
-CoInductive EqSt  : (Stream A)->(Stream A)->Prop := 
-            eqst : (s1,s2:(Stream A))
-                   (hd A s1)=(hd A s2)->
-                   (EqSt (tl A s1) (tl A s2))->(EqSt s1 s2).
+CoInductive EqSt : Stream A -> Stream A -> Prop :=
+    eqst :
+      forall s1 s2:Stream A,
+        hd A s1 = hd A s2 -> EqSt (tl A s1) (tl A s2) -> EqSt s1 s2.
 \end{coq_example}
 \noindent Now the equality of both streams can be proved introducing
 an infinite object of type 
@@ -269,10 +276,9 @@ an infinite object of type
 \noindent $(\EqSt\;s_1\;(\conc\;s_1\;s_2))$ by a \verb!CoFixpoint!
 definition.
 \begin{coq_example}
-CoFixpoint eqproof : (s1,s2:(Stream A))(EqSt s1 (conc s1 s2))
-   := [s1,s2:(Stream A)]
-        (eqst s1 (conc s1 s2)
-            (refl_equal A (hd A (conc s1 s2))) (eqproof (tl A s1) s2)).
+CoFixpoint eqproof (s1 s2:Stream A) : EqSt s1 (conc s1 s2) :=
+  eqst s1 (conc s1 s2) (refl_equal (hd A (conc s1 s2)))
+    (eqproof (tl A s1) s2).
 \end{coq_example}
 \begin{coq_eval}
 Reset eqproof.
@@ -290,23 +296,23 @@ default.
 %\pagebreak 
 
 \begin{coq_example}
-Lemma eqproof : (s1,s2:(Stream A))(EqSt s1 (conc s1 s2)).
-Cofix.
+Lemma eqproof : forall s1 s2:Stream A, EqSt s1 (conc s1 s2).
+cofix.
 \end{coq_example}
 
 \noindent An easy (and wrong!) way of finishing the proof is just to apply the
 variable \verb!eqproof!, which has the same type as the goal. 
 
 \begin{coq_example}
-Intros.
-Apply eqproof.
+intros.
+apply eqproof.
 \end{coq_example}
 
 \noindent The ``proof'' constructed in this way 
 would correspond to the \verb!CoFixpoint! definition
 \begin{coq_example*}
-CoFixpoint eqproof : (s1:(Stream A))(s2:(Stream A))(EqSt s1 (conc s1 s2))
-                   := eqproof.
+CoFixpoint eqproof  : forall s1 s2:Stream A, EqSt s1 (conc s1 s2) :=
+  eqproof.
 \end{coq_example*}
 
 \noindent which is obviously non-guarded. This means that 
@@ -334,8 +340,8 @@ applied even if the proof term is not complete.
 
 \begin{coq_example}
 Restart.
-Cofix.
-Auto. 
+cofix.
+auto.
 Guarded.
 Undo.
 Guarded.
@@ -346,17 +352,17 @@ beginning and show how to construct an admissible proof~:
 
 \begin{coq_example} 
 Restart.
-Cofix.
+ cofix.
 \end{coq_example}
 
 %\pagebreak
 
 \begin{coq_example}
-Intros.
-Apply eqst.
-Trivial.
-Simpl.
-Apply eqproof.
+intros.
+apply eqst.
+trivial.
+simpl.
+apply eqproof.
 Qed.
 \end{coq_example}
 
diff --git a/doc/RefMan-ind.tex b/doc/RefMan-ind.tex
index 6ac276d85..3389382af 100755
--- a/doc/RefMan-ind.tex
+++ b/doc/RefMan-ind.tex
@@ -72,14 +72,15 @@ Let's consider the relation \texttt{Le} over natural numbers and the
 following variables:
 
 \begin{coq_eval}
-Restore State Initial.
+Restore State "Initial".
 \end{coq_eval}
 
 \begin{coq_example*}
-Inductive Le : nat->nat->Set :=
-  LeO : (n:nat)(Le O n)  |  LeS : (n,m:nat) (Le n m)-> (Le (S n) (S m)).
-Variable P:nat->nat->Prop.
-Variable Q:(n,m:nat)(Le n m)->Prop.
+Inductive Le : nat -> nat -> Set :=
+  | LeO : forall n:nat, Le 0%N n
+  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
+Variable P : nat -> nat -> Prop.
+Variable Q : forall n m:nat, Le n m -> Prop.
 \end{coq_example*}
 
 For example purposes we defined  \verb+Le: nat->nat->Set+
@@ -105,8 +106,8 @@ it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+.
 
 For example, consider the goal:
 \begin{coq_eval}
-Lemma ex : (n,m:nat)(Le (S n) m)->(P n m).
-Intros.
+Lemma ex : forall n m:nat, Le (S n) m -> P n m.
+intros.
 \end{coq_eval}
 
 \begin{coq_example}
@@ -125,7 +126,7 @@ the constructors \texttt{LeO} and \texttt{LeS}.
 
 
 \begin{coq_example}
-Inversion_clear  H.
+inversion_clear H.
 \end{coq_example}
 
 Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
@@ -149,7 +150,7 @@ does not clear the equalities:
 Undo.
 \end{coq_example*}
 \begin{coq_example}
-Inversion H.
+inversion H.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -203,8 +204,8 @@ Note that the hypothesis \texttt{(S m0)=m} has been deduced and
 
 For example, consider the  goal:
 \begin{coq_eval}
-Lemma ex_dep : (n,m:nat)(H:(Le (S n) m))(Q (S n) m H).
-Intros.
+Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
+intros.
 \end{coq_eval}
 
 \begin{coq_example}
@@ -218,7 +219,7 @@ Neither \texttt{Inversion} nor  {\tt Inversion\_clear} make such a
 substitution. To have such a behavior we use the dependent inversion tactics:
 
 \begin{coq_example}
-Dependent Inversion_clear H.
+dependent inversion_clear H.
 \end{coq_example}
 
 Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
@@ -288,7 +289,8 @@ goal with a specified inversion lemma.
   For example, to generate the inversion lemma for the instance
  \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
 \begin{coq_example}
-Derive Inversion_clear leminv with (n,m:nat)(Le (S n) m) Sort Prop.
+Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
+ Prop.
 \end{coq_example}
 
 Let us  inspect the type of the generated lemma:
@@ -355,8 +357,8 @@ expect a predicate of type $(\vec{x}:\vec{T})s$ as first argument. \\
 \end{itemize}
 
 \begin{coq_example}
-Derive Dependent Inversion_clear leminv_dep 
-  with (n,m:nat)(Le (S n) m) Sort Prop.
+Derive Dependent Inversion_clear leminv_dep with
+ (forall n m:nat, Le (S n) m) Sort Prop.
 \end{coq_example}
 
 \begin{coq_example}
@@ -392,7 +394,7 @@ Abort.
 Show.
 \end{coq_example}
 \begin{coq_example}
-Inversion H using leminv.
+inversion H using leminv.
 \end{coq_example}
 
 
@@ -427,15 +429,18 @@ of mutual induction for objects in type {\term$_i$}.
 The definition of principle of mutual induction for {\tt tree} and
 {\tt forest} over the sort {\tt Set} is defined by the command:
 \begin{coq_eval}
-Restore State Initial.
-Variables A,B:Set.
-Mutual Inductive tree : Set :=  node : A -> forest -> tree
-with forest : Set := leaf : B -> forest 
-                   | cons : tree -> forest -> forest.
+Restore State "Initial".
+Variables A B : Set.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | leaf : B -> forest
+  | cons : tree -> forest -> forest.
 \end{coq_eval}
 \begin{coq_example*}
-Scheme tree_forest_rec := Induction for tree Sort Set 
-with forest_tree_rec := Induction for forest Sort Set.
+Scheme tree_forest_rec := Induction for tree
+  Sort Set
+  with forest_tree_rec := Induction for forest Sort Set.
 \end{coq_example*}
 You may now look at the type of {\tt tree\_forest\_rec} :
 \begin{coq_example}
@@ -464,20 +469,20 @@ natural in case of inductively defined relations.
 \Example
 With the predicates {\tt odd} and {\tt even} inductively defined as:
 \begin{coq_eval}
-Restore State Initial.
+Restore State "Initial".
 \end{coq_eval}
 \begin{coq_example*}
-Mutual Inductive odd : nat->Prop := 
-    oddS : (n:nat)(even n)->(odd (S n))
-with even : nat -> Prop := 
-    evenO : (even O) 
-  | evenS : (n:nat)(odd n)->(even (S n)).  
+Inductive odd : nat -> Prop :=
+    oddS : forall n:nat, even n -> odd (S n)
+with even : nat -> Prop :=
+  | evenO : even 0%N
+  | evenS : forall n:nat, odd n -> even (S n).
 \end{coq_example*}
 The following command generates a powerful elimination
 principle:
 \begin{coq_example*}
-Scheme odd_even := Minimality for odd Sort Prop
-with   even_odd := Minimality for even Sort Prop.
+Scheme odd_even := Minimality for   odd Sort Prop
+  with even_odd := Minimality for even Sort Prop.
 \end{coq_example*}
 The type of {\tt odd\_even} for instance will be:
 \begin{coq_example}
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 4011e975d..73731bea5 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -460,9 +460,9 @@ proof of such a lemma can be done as shown in table~\ref{cnatltac}.
 
 \begin{coq_eval}
 Reset Initial.
-Require Arith.
-Require PolyList.
-Require PolyListSyntax.
+Require Import Arith.
+Require Import PolyList.
+Require Import PolyListSyntax.
 \end{coq_eval}
 
 \begin{table}[ht]
@@ -470,15 +470,17 @@ Require PolyListSyntax.
 {\parbox{6in}
 {
 \begin{coq_example*}
-Lemma card_nat: ~(EX x:nat|(EX y:nat|(z:nat)(x=z)/\(y=z))).
+Lemma card_nat :
+ ~ ( EX x : nat | ( EX y : nat | (forall z:nat, x = z /\ y = z))).
 Proof.
-Red;Intro H.
-Elim H;Intros a Ha.
-Elim Ha;Intros b Hb.
-Elim (Hb (0));Elim (Hb (1));Elim (Hb (2));Intros;
-  Match Context With
-    [_:?1=?2;_:?1=?3|-?] ->
-      Cut ?2=?3;[Discriminate|Apply trans_equal with ?1;Auto].
+red; intro H.
+elim H; intros a Ha.
+elim Ha; intros b Hb.
+elim (Hb 0%N); elim (Hb 1%N); elim (Hb 2%N); intros;
+ match context with
+ | [_:(?X1 = ?X2),_:(?X1 = ?X3) |- _ ] =>
+     cut (X2 = X3); [ discriminate | apply trans_equal with X1; auto ]
+ end.
 Qed.
 \end{coq_example*}
 }}
@@ -504,18 +506,18 @@ First, we define the permutation predicate as shown in table~\ref{permutpred}.
 {
 \begin{coq_example*}
 Section Sort.
-Variable A:Set.
-
-Inductive permut:(list A)->(list A)->Prop:=
-  permut_refl:(l:(list A))(permut l l)
- |permut_cons:
-    (a:A)(l0,l1:(list A))(permut l0 l1)->
-      (permut (cons a l0) (cons a l1))
- |permut_append:
-    (a:A)(l:(list A))(permut (cons a l) (l^(cons a (nil A))))
- |permut_trans:
-    (l0,l1,l2:(list A))(permut l0 l1)->(permut l1 l2)->
-      (permut l0 l2).
+Variable A : Set.
+Inductive permut : 
+list A -> list A -> Prop :=
+  | permut_refl : forall l:list A, permut l l
+  | permut_cons :
+      forall (a:A) (l0 l1:list A),
+        permut l0 l1 -> permut (a :: l0) (a :: l1)
+  | permut_append :
+      forall (a:A) (l:list A), permut (a :: l) (l ^ a :: nil)
+  | permut_trans :
+      forall l0 l1 l2:list A,
+        permut l0 l1 -> permut l1 l2 -> permut l0 l2.
 End Sort.
 \end{coq_example*}
 }}
@@ -550,26 +552,29 @@ Compute in} and we can get the terms back by {\tt Match}.
 {\parbox{6in}
 {
 \begin{coq_example}
-Recursive Tactic Definition Permut n:=
- Match Context With
-   [|-(permut ? ?1 ?1)] -> Apply permut_refl
-  |[|-(permut ? (cons ?1 ?2) (cons ?1 ?3))] ->
-     Let newn=Eval Compute in (length ?2) In
-     Apply permut_cons;(Permut newn)
-  |[|-(permut ?1 (cons ?2 ?3) ?4)] ->
-     (Match Eval Compute in n With
-        [(1)] -> Fail
-       |_ ->
-         Let l0'='(?3^(cons ?2 (nil ?1))) In
-         Apply (permut_trans ?1 (cons ?2 ?3) l0' ?4);
-         [Apply permut_append|
-          Compute;(Permut '(pred n))]).
-
-Tactic Definition PermutProve:=
- Match Context With
-   [|-(permut ? ?1 ?2)] ->
-     (Match Eval Compute in ((length ?1)=(length ?2)) With
-        [?1=?1] -> (Permut ?1)).
+Ltac Permut n :=
+  match context with
+  | [ |- (permut _ ?X1 ?X1) ] => apply permut_refl
+  | [ |- (permut _ (?X1 :: ?X2) (?X1 :: ?X3)) ] =>
+      let newn := eval compute in (length X2) in
+      (apply permut_cons; Permut newn)
+  | [ |- (permut ?X1 (?X2 :: ?X3) ?X4) ] =>
+      match eval compute in n with
+      | [1%N] => fail
+      | _ =>
+          let l0' := '(X3 ^ X2 :: nil) in
+          (apply (permut_trans X1 (X2 :: X3) l0' X4);
+            [ apply permut_append | compute; Permut (pred n) ])
+      end
+  end.
+Ltac PermutProve :=
+  match context with
+  | [ |- (permut _ ?X1 ?X2) ] =>
+      match eval compute in 
+            (length X1 = length X2) with
+      | [(?X1 = ?X1)] => Permut X1
+      end
+  end.
 \end{coq_example}
 }}
 \caption{Permutation tactic}
@@ -584,22 +589,23 @@ table~\ref{permutlem}.
 {\parbox{6in}
 {
 \begin{coq_example*}
-Lemma permut_ex1:
-  (permut nat (cons (1) (cons (2) (cons (3) (nil nat))))
-     (cons (3) (cons (2) (cons (1) (nil nat))))).
+Lemma permut_ex1 :
+ permut nat (1%N :: 2%N :: 3%N :: nil) (3%N :: 2%N :: 1%N :: nil).
 Proof.
 PermutProve.
-Save.
-
-Lemma permut_ex2:
- (permut nat
-   (cons (0) (cons (1) (cons (2) (cons (3) (cons (4) (cons (5)
-     (cons (6) (cons (7) (cons (8) (cons (9) (nil nat)))))))))))
-   (cons (0) (cons (2) (cons (4) (cons (6) (cons (8) (cons (9)
-     (cons (7) (cons (5) (cons (3) (cons (1) (nil nat)))))))))))).
+Qed.
+Lemma permut_ex2 :
+ 
+ permut nat
+   (0%N
+    :: 1%N
+       :: 2%N :: 3%N :: 4%N :: 5%N :: 6%N :: 7%N :: 8%N :: 9%N :: nil)
+   (0%N
+    :: 2%N
+       :: 4%N :: 6%N :: 8%N :: 9%N :: 7%N :: 5%N :: 3%N :: 1%N :: nil).
 Proof.
 PermutProve.
-Save.
+Qed.
 \end{coq_example*}
 }}
 \caption{Examples of {\tt PermutProve} use}
@@ -625,46 +631,56 @@ for the left implication to get rid of the contraction and the right or).
 {\parbox{6in}
 {
 \begin{coq_example}
-Tactic Definition Axioms:=
-  Match Context With
-   [|-True] -> Trivial
-  |[_:False|- ?] -> ElimType False;Assumption
-  |[_:?1|-?1] -> Auto.
-
-Tactic Definition DSimplif:=
- Repeat
-  (Intros;
-   (Match Context With
-     [id:~?|-?] -> Red in id
-    |[id:?/\?|-?] -> Elim id;Do 2 Intro;Clear id
-    |[id:?\/?|-?] -> Elim id;Intro;Clear id
-    |[id:?1/\?2->?3|-?] ->
-       Cut ?1->?2->?3;[Intro|Intros;Apply id;Split;Assumption]
-    |[id:?1\/?2->?3|-?] ->
-       Cut ?2->?3;[Cut ?1->?3;[Intros|
-                               Intro;Apply id;Left;Assumption]|
-                   Intro;Apply id;Right;Assumption]
-    |[id0:?1->?2;id1:?1|-?] ->
-       Cut ?2;[Intro;Clear id0|Apply id0;Assumption]
-    |[|-?/\?] -> Split
-    |[|-~?] -> Red)).
-
-Recursive Tactic Definition TautoProp:=
+Ltac Axioms :=
+  match context with
+  | [ |- True ] => trivial
+  | [_:False |- _ ] => elimtype False; assumption
+  | [_:?X1 |- ?X1 ] => auto
+  end.
+Ltac DSimplif :=
+  repeat
+   (
+     intros;
+     match context with
+     | [id:(~ _) |- _ ] => red in id
+     | [id:(_ /\ _) |- _ ] =>
+         elim id; do 2 intro; clear id
+     | [id:(_ \/ _) |- _ ] =>
+         elim id; intro; clear id
+     | [id:(?X1 /\ ?X2 -> ?X3) |- _ ] =>
+         cut (X1 -> X2 -> X3);
+          [ intro | intros; apply id; split; assumption ]
+     | [id:(?X1 \/ ?X2 -> ?X3) |- _ ] =>
+         cut (X2 -> X3);
+          [ cut (X1 -> X3);
+             [ intros | intro; apply id; left; assumption ]
+          | intro; apply id; right; assumption ]
+     | [id0:(?X1 -> ?X2),id1:?X1 |- _ ] =>
+         cut X2; [ intro; clear id0 | apply id0; assumption ]
+     | [ |- (_ /\ _) ] => split
+     | [ |- (~ _) ] => red
+     end).
+Ltac TautoProp :=
   DSimplif;
-   Axioms
-   Orelse
-   Match Context With
-    [id:(?1->?2)->?3|-?] ->
-      Cut ?2->?3;[Intro;Cut ?1->?2;[Intro;Cut ?3;[Intro;Clear id|
-                              Apply id;Assumption]|Clear id]|
-                  Intro;Apply id;Intro;Assumption];TautoProp
-   |[id:~?1->?2|-?]->
-      Cut False->?2;
-      [Intro;Cut ?1->False;[Intro;Cut ?2;[Intro;Clear id|
-                               Apply id;Assumption]|Clear id]|
-       Intro;Apply id;Red;Intro;Assumption];TautoProp
-   |[|-?\/?] ->
-      (Left;TautoProp) Orelse (Right;TautoProp).
+   Axioms ||
+     match context with
+     | [id:((?X1 -> ?X2) -> ?X3) |- _ ] =>
+         
+          cut (X2 -> X3);
+          [ intro; cut (X1 -> X2);
+             [ intro; cut X3;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; intro; assumption ]; TautoProp
+     | [id:(~ ?X1 -> ?X2) |- _ ] =>
+         cut (False -> X2);
+          [ intro; cut (X1 -> False);
+             [ intro; cut X2;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; red; intro; assumption ]; TautoProp
+     | [ |- (_ \/ _) ] => (left; TautoProp) || (right; TautoProp)
+     end.
 \end{coq_example}
 }}
 \caption{Deciding intuitionistic propositions}
@@ -679,15 +695,16 @@ table~\ref{tautolem}.
 {\parbox{6in}
 {
 \begin{coq_example*}
-Lemma tauto_ex1:(A,B:Prop)A/\B->A\/B.
+Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
 Proof.
 TautoProp.
-Save.
-
-Lemma tauto_ex2:(A,B:Prop)(~~B->B)->(A->B)->~~A->B.
+Qed.
+Lemma tauto_ex2 :
+ 
+ forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
 Proof.
 TautoProp.
-Save.
+Qed.
 \end{coq_example*}
 }}
 \caption{Proofs of tautologies with {\tt TautoProp}}
@@ -708,26 +725,25 @@ table~\ref{isosax}.
 {
 \begin{coq_eval}
 Reset Initial.
-Require Arith.
+Require Import Arith.
 \end{coq_eval}
 \begin{coq_example*}
 Section Iso_axioms.
-
-Variable A,B,C:Set.
-
-Axiom Com:(A*B)==(B*A).
-Axiom Ass:(A*(B*C))==((A*B)*C).
-Axiom Cur:((A*B)->C)==(A->B->C).
-Axiom Dis:(A->(B*C))==((A->B)*(A->C)).
-Axiom P_unit:(A*unit)==A.
-Axiom AR_unit:(A->unit)==unit.
-Axiom AL_unit:(unit->A)==A.
-
-Lemma Cons:B==C->(A*B)==(A*C).
+Variables A B C : 
+            Set.
+Axiom Com : 
+        A * B = B * A.
+Axiom Ass : A * (B * C) = A * B * C.
+Axiom Cur : (A * B -> C) = (A -> B -> C).
+Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
+Axiom P_unit : A * unit = A.
+Axiom AR_unit : (A -> unit) = unit.
+Axiom AL_unit : (unit -> A) = A.
+Lemma Cons : 
+ B = C -> A * B = A * C.
 Proof.
-Intro Heq;Rewrite Heq;Apply refl_eqT.
-Save.
-
+intro Heq; rewrite Heq; apply refl_equal.
+Qed.
 End Iso_axioms.
 \end{coq_example*}
 }}
@@ -749,33 +765,41 @@ CompareStruct}). The main tactic to be called and realizing this algorithm is
 {\parbox{6in}
 {
 \begin{coq_example}
-Recursive Tactic Definition DSimplif trm:=
-  Match trm With
-   [(?1*?2)*?3] -> Rewrite <- (Ass ?1 ?2 ?3);Try MainSimplif
-  |[(?1*?2)->?3] -> Rewrite (Cur ?1 ?2 ?3);Try MainSimplif
-  |[?1->(?2*?3)] -> Rewrite (Dis ?1 ?2 ?3);Try MainSimplif
-  |[?1*unit] -> Rewrite (P_unit ?1);Try MainSimplif
-  |[unit*?1] -> Rewrite (Com unit ?1);Try MainSimplif
-  |[?1->unit] -> Rewrite (AR_unit ?1);Try MainSimplif
-  |[unit-> ?1] -> Rewrite (AL_unit ?1);Try MainSimplif
-  |[?1*?2] ->
-     ((DSimplif ?1);Try MainSimplif) Orelse
-     ((DSimplif ?2);Try MainSimplif)
-  |[?1-> ?2] ->
-     ((DSimplif ?1);Try MainSimplif) Orelse
-     ((DSimplif ?2);Try MainSimplif)
-And MainSimplif:=
-  Match Context With
-   [|- ?1== ?2] -> Try (DSimplif ?1);Try (DSimplif ?2).
-
-Recursive Tactic Definition Length trm:=
-  Match trm With
-   [?*?1] ->
-     Let succ=(Length ?1) In
-     '(S succ)
-  |_ -> '(1).
-
-Tactic Definition Assoc:= Repeat Rewrite <- Ass.
+Ltac DSimplif trm :=
+  match 
+  trm with
+  | [(?X1 * ?X2 * ?X3)] =>
+      rewrite <- (Ass X1 X2 X3); try MainSimplif
+  | [(?X1 * ?X2 -> ?X3)] =>
+      rewrite (Cur X1 X2 X3); try MainSimplif
+  | [(?X1 -> ?X2 * ?X3)] =>
+      rewrite (Dis X1 X2 X3); try MainSimplif
+  | [(?X1 * unit)] =>
+      rewrite (P_unit X1); try MainSimplif
+  | [(unit * ?X1)] =>
+      rewrite (Com unit X1); try MainSimplif
+  | [(?X1 -> unit)] =>
+      rewrite (AR_unit X1); try MainSimplif
+  | [(unit -> ?X1)] =>
+      rewrite (AL_unit X1); try MainSimplif
+  | [(?X1 * ?X2)] =>
+      (DSimplif X1; try MainSimplif) || (DSimplif X2; try MainSimplif)
+  | [(?X1 -> ?X2)] =>
+      (DSimplif X1; try MainSimplif) || (DSimplif X2; try MainSimplif)
+  end
+ with MainSimplif :=
+  match context with
+  | [ |- (?X1 = ?X2) ] => try DSimplif X1; try DSimplif X2
+  end.
+Ltac Length trm :=
+  match 
+  trm with
+  | [(_ * ?X1)] => let succ := Length X1 in
+                   '(S succ)
+  | _ => '1%N
+  end.
+Ltac assoc := repeat 
+               rewrite <- Ass.
 \end{coq_example}
 }}
 \caption{Type isomorphism tactic (1)}
@@ -787,29 +811,29 @@ Tactic Definition Assoc:= Repeat Rewrite <- Ass.
 {\parbox{6in}
 {
 \begin{coq_example}
-Recursive Tactic Definition DoCompare n:=
-  Match Context With
-   [|-?1==?1] -> Apply refl_eqT
-  |[|-(?1*?2)==(?1*?3)] ->
-     Apply Cons;
-     Let newn=(Length ?2) In
-     (DoCompare newn)
-  |[|-(?1*?2)==?3] ->
-     (Match Eval Compute in n With
-       [(1)] -> Fail
-      |_ -> 
-        Pattern 1 (?1*?2);Rewrite Com;Assoc;
-        (DoCompare '(pred n))).
-
-Tactic Definition CompareStruct:=
-  Match Context With
-   [|-?1==?2] ->
-     Let l1=(Length ?1)
-     And l2=(Length ?2) In
-     (Match Eval Compute in l1=l2 With
-        [?1=?1] -> (DoCompare ?1)).
-
-Tactic Definition IsoProve:=MainSimplif;CompareStruct.
+Ltac DoCompare n :=
+  match context with
+  | [ |- (?X1 = ?X1) ] => apply refl_equal
+  | [ |- (?X1 * ?X2 = ?X1 * ?X3) ] =>
+      apply Cons; let newn := Length X2 in
+                  DoCompare newn
+  | [ |- (?X1 * ?X2 = ?X3) ] =>
+      match eval compute in n with
+      | [1%N] => fail
+      | _ =>
+          pattern (X1 * X2) 1; rewrite Com; assoc; DoCompare (pred n)
+      end
+  end.
+Ltac CompareStruct :=
+  match context with
+  | [ |- (?X1 = ?X2) ] =>
+      let l1 := 
+      Length X1 with l2 := Length X2 in
+      match eval compute in (l1 = l2) with
+      | [(?X1 = ?X1)] => DoCompare X1
+      end
+  end.
+Ltac IsoProve := MainSimplif; CompareStruct.
 \end{coq_example}
 }}
 \caption{Type isomorphism tactic (2)}
@@ -823,17 +847,19 @@ Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
 {\parbox{6in}
 {
 \begin{coq_example*}
-Lemma isos_ex1:(A,B:Set)((A*unit)*B)==(B*(unit*A)).
+Lemma isos_ex1 : 
+ forall A B:Set, A * unit * B = B * (unit * A).
 Proof.
-Intros;IsoProve.
-Save.
-
-Lemma isos_ex2:(A,B,C:Set)
-  ((A*unit)->(B*C*unit))==
-  (((A*unit)->((C->unit)*C))*(unit->(A->B))).
+intros; IsoProve.
+Qed.
+Lemma isos_ex2 :
+ 
+ forall A B C:Set,
+   (A * unit -> B * (C * unit)) =
+   (A * unit -> (C -> unit) * C) * (unit -> A -> B).
 Proof.
-Intros;IsoProve.
-Save.
+intros; IsoProve.
+Qed.
 \end{coq_example*}
 }}
 \caption{Type equalities solved by {\tt IsoProve}}