Traduction de syntaxe vers ltac

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

1 files changed, 15 insertions, 16 deletions

diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 6b7ffca5e..9895af8ae 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -61,36 +61,35 @@ CoInductive EqSt  : Stream->Stream->Prop :=
 
 (* A coinduction principle *)
 
-Tactic Definition CoInduction [$proof] := 
-       [ <:tactic:<( Cofix $proof; (Intros; (Constructor;
-                    [Clear $proof | Try (Apply $proof;Clear $proof)])))>> ].
+Tactic Definition CoInduction proof := 
+  Cofix proof; Intros; Constructor;
+    [Clear proof | Try '(Apply proof;Clear proof)].
 
 
 (* Extensional equality is an equivalence relation *)
 
-
 Theorem  EqSt_reflex : (s:Stream)(EqSt s s).
-CoInduction EqSt_reflex.
+'(CoInduction EqSt_reflex).
 Reflexivity.
 Qed.
 
 Theorem sym_EqSt : 
  (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1).
-CoInduction Eq_sym.
-(Case H;Intros;Symmetry;Assumption).
-(Case H;Intros;Assumption).
+'(CoInduction Eq_sym).
+Case H;Intros;Symmetry;Assumption.
+Case H;Intros;Assumption.
 Qed.
 
 
 Theorem trans_EqSt : 
  (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3).
-CoInduction Eq_trans.
+'(CoInduction Eq_trans).
 Transitivity (hd s2).
-(Case H; Intros; Assumption).
-(Case H0; Intros; Assumption).
+Case H; Intros; Assumption.
+Case H0; Intros; Assumption.
 Apply (Eq_trans (tl s1) (tl s2) (tl s3)).
-(Case H;  Trivial with datatypes).
-(Case H0; Trivial with datatypes).
+Case H;  Trivial with datatypes.
+Case H0; Trivial with datatypes.
 Qed.
 
 (* 
@@ -105,12 +104,12 @@ Intros m hypind.
 Simpl.
 Intros s1 s2 H.
 Apply hypind.
-(Case H; Trivial with datatypes).
+Case H; Trivial with datatypes.
 Qed.
 
 Theorem ntheq_eqst : 
   (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2).
-CoInduction Equiv2.
+'(CoInduction Equiv2).
 Apply (H O).
 Intros n; Apply (H (S n)).
 Qed.
@@ -139,7 +138,7 @@ Hypothesis InvThenP   : (x:Stream)(Inv x)->(P x).
 Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)).
 
 Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x).
-CoInduction ForAll_coind;Auto.
+'(CoInduction ForAll_coind);Auto.
 Qed.
 End Co_Induction_ForAll.