Fix the test-suite by removing any Reset in the scripts

 Reset and the other backtracking commands (Back, BackTo, Backtrack)
 are now allowed only during interactive session, not in compiled
 or loaded scripts.

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

1 files changed, 16 insertions, 6 deletions

diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index d3b7cf3f3..bfead53c0 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -222,7 +222,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci.
  de l'arite de chaque operateur *)
 
 
-Section Sig.
+Module Sig.
 
 Record Signature : Type :=
   {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}.
@@ -277,7 +277,7 @@ Type
   | _, _ => False
   end.
 
-
+Module Type Version1.
 
 Definition equalT (t1 t2 : TERM) : Prop :=
   match t1, t2 with
@@ -294,12 +294,15 @@ Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint)
   | _, _ => False
   end.
 
+End Version1.
+
 
-Reset equalT.
 (* ------------------------------------------------------------------*)
 (*          Initial exemple (without patterns)                       *)
 (*-------------------------------------------------------------------*)
 
+Module Version2.
+
 Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
   match t1 return (TERM -> Prop) with
   | var v1 =>
@@ -347,11 +350,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
       end
   end.
 
+End Version2.
 
 (* ---------------------------------------------------------------- *)
 (*                Version with simple patterns                      *)
 (* ---------------------------------------------------------------- *)
-Reset equalT.
+
+Module Version3.
 
 Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
   match t1 with
@@ -388,8 +393,9 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
       end
   end.
 
+End Version3.
 
-Reset equalT.
+Module Version4.
 
 Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
   match t1 with
@@ -423,10 +429,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
       end
   end.
 
+End Version4.
+
 (* ---------------------------------------------------------------- *)
 (*                  Version with multiple patterns                  *)
 (* ---------------------------------------------------------------- *)
-Reset equalT.
+
+Module Version5.
 
 Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop :=
   match t1, t2 with
@@ -445,6 +454,7 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop :=
   | _, _ => False
   end.
 
+End Version5.
 
 (* ------------------------------------------------------------------ *)