1 files changed, 46 insertions, 25 deletions

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 745529bf..f445ca8e 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                             *)