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, 46 insertions, 25 deletions

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 745529bf6..f445ca8ea 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -100,7 +100,7 @@ Type (fun x : nat => match x return nat with
                      | x => x
                      end).
 
-Section testlist.
+Module Type testlist.
 Parameter A : Set.
 Inductive list : Set :=
   | nil : list
@@ -119,7 +119,6 @@ Definition titi (a : A) (l : list) :=
   | nil => l
   | cons b l => l
   end.
-Reset list.
 End testlist.
 
 
@@ -913,71 +912,77 @@ Type
    | LeS n m _ => (S n, S m)
    end).
 
-
+Module Type F_v1.
 Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
   match h in (Le n m) return (Le n (S m)) with
   | LeO m' => LeO (S m')
   | LeS n' m' h' => LeS n' (S m') (F n' m' h')
   end.
+End F_v1.
 
-Reset F.
-
+Module Type F_v2.
 Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
   match h in (Le n m) return (Le n (S m)) with
   | LeS n m h => LeS n (S m) (F n m h)
   | LeO m => LeO (S m)
   end.
+End F_v2.
 
 (* Rend la longueur de la liste *)
-Definition length1 (n : nat) (l : listn n) :=
+
+Module Type L1.
+Definition length (n : nat) (l : listn n) :=
   match l return nat with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => 1
   | _ => 0
   end.
+End L1.
 
-Reset length1.
-Definition length1 (n : nat) (l : listn n) :=
+Module Type L1'.
+Definition length (n : nat) (l : listn n) :=
   match l with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => 1
   | _ => 0
   end.
+End L1'.
 
-
-Definition length2 (n : nat) (l : listn n) :=
+Module Type L2.
+Definition length (n : nat) (l : listn n) :=
   match l return nat with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => S n
   | _ => 0
   end.
+End L2.
 
-Reset length2.
-
-Definition length2 (n : nat) (l : listn n) :=
+Module Type L2'.
+Definition length (n : nat) (l : listn n) :=
   match l with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => S n
   | _ => 0
   end.
+End L2'.
 
-Definition length3 (n : nat) (l : listn n) :=
+Module Type L3.
+Definition length (n : nat) (l : listn n) :=
   match l return nat with
   | consn n _ (consn m _ l) => S n
   | consn n _ _ => 1
   | _ => 0
   end.
+End L3.
 
-
-Reset length3.
-
-Definition length3 (n : nat) (l : listn n) :=
+Module Type L3'.
+Definition length (n : nat) (l : listn n) :=
   match l with
   | consn n _ (consn m _ l) => S n
   | consn n _ _ => 1
   | _ => 0
   end.
-
+End L3'.
 
 Type match LeO 0 return nat with
      | LeS n m h => n + m
@@ -1256,7 +1261,7 @@ Type match (0, 0) with
      | (x, y) => (S x, S y)
      end.
 
-
+Module Type test_concat.
 
 Parameter concat : forall A : Set, List A -> List A -> List A.
 
@@ -1273,6 +1278,7 @@ Type
   | _, _ => Nil nat
   end.
 
+End test_concat.
 
 Inductive redexes : Set :=
   | VAR : nat -> redexes
@@ -1295,7 +1301,6 @@ Type (fun n : nat => match n with
                      | _ => 0
                      end).
 
-Reset concat.
 Parameter
   concat :
     forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m).
@@ -1383,6 +1388,7 @@ Type
 (* I.e. to test manipulation of elimination predicate                    *)
 (* ===================================================================== *)
 
+Module Type test_term.
 
 Parameter LTERM : nat -> Set.
 Inductive TERM : Type :=
@@ -1397,7 +1403,8 @@ Type
   | oper op1 l1, oper op2 l2 => False
   | _, _ => False
   end.
-Reset LTERM.
+
+End test_term.
 
 
 
@@ -1493,6 +1500,7 @@ Type
   end.
 
 
+Module Type ff.
 
 Parameter ff : forall n m : nat, n <> m -> S n <> S m.
 Parameter discr_r : forall n : nat, 0 <> S n.
@@ -1505,6 +1513,7 @@ Type
    | S x => or_intror (S x = 0) (discr_l x)
    end).
 
+Module Type eqdec.
 
 Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
   match n, m return (n = m \/ n <> m) with
@@ -1518,7 +1527,9 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
       end
   end.
 
-Reset eqdec.
+End eqdec.
+
+Module Type eqdec'.
 
 Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
   match n return (forall m : nat, n = m \/ n <> m) with
@@ -1540,6 +1551,7 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
       end
   end.
 
+End eqdec'.
 
 Inductive empty : forall n : nat, listn n -> Prop :=
     intro_empty : empty 0 niln.
@@ -1554,7 +1566,10 @@ Type
    | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
    end).
 
-Reset ff.
+End ff.
+
+Module Type ff'.
+
 Parameter ff : forall n m : nat, n <> m -> S n <> S m.
 Parameter discr_r : forall n : nat, 0 <> S n.
 Parameter discr_l : forall n : nat, S n <> 0.
@@ -1566,6 +1581,7 @@ Type
    | S x => or_intror (S x = 0) (discr_l x)
    end).
 
+Module Type eqdec.
 
 Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
   match n, m return (n = m \/ n <> m) with
@@ -1578,7 +1594,10 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
       | or_intror h => or_intror (S x = S y) (ff x y h)
       end
   end.
-Reset eqdec.
+
+End eqdec.
+
+Module Type eqdec'.
 
 Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
   match n return (forall m : nat, n = m \/ n <> m) with
@@ -1600,6 +1619,8 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
       end
   end.
 
+End eqdec'.
+End ff'.
 
 (* ================================================== *)
 (* Pour tester parametres                             *)