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

8 files changed, 129 insertions, 141 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                             *)
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.
 
 (* ------------------------------------------------------------------ *)
 
diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v
index 74228bbbf..515161660 100644
--- a/test-suite/success/Mod_params.v
+++ b/test-suite/success/Mod_params.v
@@ -20,59 +20,31 @@ End Q.
 #trace Nametab.exists_cci;;
 *)
 
-Module M.
-Reset M.
-Module M (X: SIG).
-Reset M.
-Module M (X Y: SIG).
-Reset M.
-Module M (X: SIG) (Y: SIG).
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG).
-Reset M.
-Module M (X: SIG) (Y: SIG).
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG).
-Reset M.
-Module M : SIG.
-Reset M.
-Module M (X: SIG) : SIG.
-Reset M.
-Module M (X Y: SIG) : SIG.
-Reset M.
-Module M (X: SIG) (Y: SIG) : SIG.
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG) : SIG.
-Reset M.
-Module M (X: SIG) (Y: SIG) : SIG.
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG) : SIG.
-Reset M.
-Module M := F Q.
-Reset M.
-Module M (X: FSIG) := X Q.
-Reset M.
-Module M (X Y: FSIG) := X Q.
-Reset M.
-Module M (X: FSIG) (Y: SIG) := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) := X Z.
-Reset M.
-Module M (X: FSIG) (Y: SIG) := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) := X Z.
-Reset M.
-Module M : SIG := F Q.
-Reset M.
-Module M (X: FSIG) : SIG := X Q.
-Reset M.
-Module M (X Y: FSIG) : SIG := X Q.
-Reset M.
-Module M (X: FSIG) (Y: SIG) : SIG := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
-Reset M.
-Module M (X: FSIG) (Y: SIG) : SIG := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
-Reset M.
+Module M01. End M01.
+Module M02 (X: SIG). End M02.
+Module M03 (X Y: SIG). End M03.
+Module M04 (X: SIG) (Y: SIG). End M04.
+Module M05 (X Y: SIG) (Z1 Z: SIG). End M05.
+Module M06 (X: SIG) (Y: SIG). End M06.
+Module M07 (X Y: SIG) (Z1 Z: SIG). End M07.
+Module M08 : SIG. End M08.
+Module M09 (X: SIG) : SIG. End M09.
+Module M10 (X Y: SIG) : SIG. End M10.
+Module M11 (X: SIG) (Y: SIG) : SIG. End M11.
+Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12.
+Module M13 (X: SIG) (Y: SIG) : SIG. End M13.
+Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14.
+Module M15 := F Q.
+Module M16 (X: FSIG) := X Q.
+Module M17 (X Y: FSIG) := X Q.
+Module M18 (X: FSIG) (Y: SIG) := X Y.
+Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z.
+Module M20 (X: FSIG) (Y: SIG) := X Y.
+Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z.
+Module M22 : SIG := F Q.
+Module M23 (X: FSIG) : SIG := X Q.
+Module M24 (X Y: FSIG) : SIG := X Q.
+Module M25 (X: FSIG) (Y: SIG) : SIG := X Y.
+Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
+Module M27 (X: FSIG) (Y: SIG) : SIG := X Y.
+Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 3c34ff928..89f110593 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -17,10 +17,12 @@ Check (nat |= nat --> nat).
 (* Check that first non empty definition at an empty level can be of any
    associativity *)
 
-Definition marker := O.
+Module Type v1.
 Notation "x +1" := (S x) (at level 8, left associativity).
-Reset marker.
+End v1.
+Module Type v2.
 Notation "x +1" := (S x) (at level 8, right associativity).
+End v2.
 
 (* Check that empty levels (here 8 and 2 in pattern) are added in the
    right order *)
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 2602c7e35..64048fe24 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1,3 +1,5 @@
+Module Type LocalNat.
+
 Inductive nat : Set :=
  | O : nat
  | S : nat->nat.
@@ -5,7 +7,8 @@ Check nat.
 Check O.
 Check S.
 
-Reset nat.
+End LocalNat.
+
 Print nat.
 
 
@@ -477,10 +480,10 @@ Qed.
 
 
 
-(*
 
-Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
+Fail Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
       match p with exP_intro X HX => X end).
+(*
 Error:
 Incorrect elimination of "p" in the inductive type
 "ex_Prop", the return type has sort "Type" while it should be
@@ -489,12 +492,11 @@ Incorrect elimination of "p" in the inductive type
 Elimination of an inductive object of sort "Prop"
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs
-
 *)
 
-(*
-Check (match prop_inject with (prop_intro P p) => P end).
 
+Fail Check (match prop_inject with (prop_intro p) => p end).
+(*
 Error:
 Incorrect elimination of "prop_inject" in the inductive type
 "prop", the return type has sort "Type" while it should be
@@ -503,13 +505,12 @@ Incorrect elimination of "prop_inject" in the inductive type
 Elimination of an inductive object of sort "Prop"
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs
-
 *)
 Print prop_inject.
 
 (*
 prop_inject =
-prop_inject = prop_intro prop (fun H : prop => H)
+prop_inject = prop_intro prop
      : prop
 *)
 
@@ -520,26 +521,24 @@ Inductive  typ : Type :=
 Definition typ_inject: typ.
 split.
 exact typ.
+Fail Defined.
 (*
-Defined.
-
 Error: Universe Inconsistency.
 *)
 Abort.
-(*
 
-Inductive aSet : Set :=
+Fail Inductive aSet : Set :=
   aSet_intro: Set -> aSet.
-
-
+(*
 User error: Large non-propositional inductive types must be in Type
-
 *)
 
 Inductive ex_Set  (P : Set -> Prop) : Type :=
   exS_intro : forall X : Set, P X -> ex_Set P.
 
 
+Module Type Version1.
+
 Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
   c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
 
@@ -553,21 +552,15 @@ Goal ~(comes_from_the_left _ _ (or_intror True I)).
  *)
 Abort.
 
-Reset comes_from_the_left.
-
-(*
+End Version1.
 
-
-
-
-
-
- Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
+Fail Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
   match H with
          |  or_introl p => True
          |  or_intror q => False
   end.
 
+(*
 Error:
 Incorrect elimination of "H" in the inductive type
 "or", the return type has sort "Type" while it should be
@@ -576,7 +569,6 @@ Incorrect elimination of "H" in the inductive type
 Elimination of an inductive object of sort "Prop"
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs
-
 *)
 
 Definition comes_from_the_left_sumbool
@@ -737,6 +729,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat :=
           | S m => plus'' m (S p)
  end.
 
+Module Type even_test_v1.
 
 Fixpoint even_test (n:nat) : bool :=
   match n
@@ -745,8 +738,9 @@ Fixpoint even_test (n:nat) : bool :=
      | S (S p) => even_test p
   end.
 
+End even_test_v1.
 
-Reset even_test.
+Module even_test_v2.
 
 Fixpoint even_test (n:nat) : bool :=
   match n
@@ -761,12 +755,8 @@ with odd_test (n:nat) : bool :=
      | S p => even_test p
  end.
 
-
-
 Eval simpl in even_test.
 
-
-
 Eval simpl in (fun x : nat => even_test x).
 
 Eval simpl in (fun x : nat => plus 5 x).
@@ -774,6 +764,8 @@ Eval simpl in (fun x : nat => even_test (plus 5 x)).
 
 Eval simpl in (fun x : nat => even_test (plus x 5)).
 
+End even_test_v2.
+
 
 Section Principle_of_Induction.
 Variable    P               : nat -> Prop.
@@ -866,14 +858,13 @@ Print Acc.
 
 Require Import Minus.
 
-(*
-Fixpoint div (x y:nat){struct x}: nat :=
+Fail Fixpoint div (x y:nat){struct x}: nat :=
  if eq_nat_dec x 0
   then 0
   else if eq_nat_dec y 0
        then x
        else S (div (x-y) y).
-
+(*
 Error:
 Recursive definition of div is ill-formed.
 In environment
@@ -971,19 +962,15 @@ Proof.
  intros A v;inversion v.
 Abort.
 
-(*
- Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
-                                  n= 0 -> v = Vnil A.
 
-Toplevel input, characters 40281-40287
-> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),                                    n= 0 -> v = Vnil A.
->                                                                                                                 ^^^^^^
+Fail Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+                                  n= 0 -> v = Vector.nil A.
+(*
 Error: In environment
 A : Set
 n : nat
 v : Vector.t A n
-e : n = 0
-The term "Vnil A" has type "Vector.t A 0" while it is expected to have type
+The term "[]" has type "Vector.t A 0" while it is expected to have type
  "Vector.t A n"
 *)
  Require Import JMeq.
diff --git a/test-suite/success/Reset.v b/test-suite/success/Reset.v
deleted file mode 100644
index b71ea69d7..000000000
--- a/test-suite/success/Reset.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Check Reset Section *)
-
-Section A.
-Definition B := Prop.
-End A.
-
-Reset A.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 8e829e061..d3c761019 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -97,13 +97,14 @@ Qed.
 
 (* Check use of unification of bindings types in specialize *)
 
+Module Type Test.
 Variable P : nat -> Prop.
 Variable L : forall (l : nat), P l -> P l.
 Goal P 0 -> True.
 intros.
 specialize L with (1:=H).
 Abort.
-Reset P.
+End Test.
 
 (* Two examples that show that hnf_constr is used when unifying types
    of bindings (a simplification of a script from Field_Theory) *)
diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v
index af81e53d6..ebd90a40e 100644
--- a/test-suite/success/hyps_inclusion.v
+++ b/test-suite/success/hyps_inclusion.v
@@ -19,14 +19,16 @@ red in H.
 (* next tactic was failing wrt bug #1325 because type-checking the goal
    detected a syntactically different type for the section variable H *)
 case 0.
-Reset A.
+Abort.
+End A.
 
 (* Variant with polymorphic inductive types for bug #1325 *)
 
-Section A.
+Section B.
 Variable H:not True.
 Inductive I (n:nat) : Type := C : H=H -> I n.
 Goal I 0.
 red in H.
 case 0.
-Reset A.
+Abort.
+End B.