3 files changed, 79 insertions, 9 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 71d33177..6198f29a 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -27,13 +27,13 @@ Module Pair (X: PO) (Y: PO) <: PO.
   Qed.
 
   Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
-    unfold le in |- *;  intuition; info  eauto.
+    unfold le;  intuition; info  eauto.
   Qed.
 
   Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
     destruct p1.
     destruct p2.
-    unfold le in |- *.
+    unfold le.
      intuition.
      cutrewrite (t = t1).
      cutrewrite (t0 = t2).
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index e3694b81..341805a1 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -66,7 +66,7 @@ Module FuncDict (E: ELEM).
   Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
 
     intros.
-    unfold find, add in |- *.
+    unfold find, add.
     elim (Reflexivity_provable _ _ (E.eq_dec e e)).
     intros.
      rewrite H.
@@ -77,13 +77,13 @@ Module FuncDict (E: ELEM).
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
     intros.
-    unfold add, find in |- *.
+    unfold add, find.
     cut (exists x : _, E.eq_dec e' e = right _ x).
     intros.
     elim H0.
     intros.
      rewrite H1.
-    unfold ifte in |- *.
+    unfold ifte.
     reflexivity.
 
     apply Disequality_provable.
@@ -123,7 +123,7 @@ Module Lemmas (G: SET) (E: ELEM).
    forall a : E.T, ESet.find a S1 = ESet.find a S2.
 
     intros.
-    unfold S1, S2 in |- *.
+    unfold S1, S2.
     elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
      try  rewrite <- H1; try  rewrite <- H2;
      repeat
@@ -153,7 +153,7 @@ Module ListDict (E: ELEM).
 
   Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
     intros.
-    simpl in |- *.
+    simpl.
     elim (Reflexivity_provable _ _ (E.eq_dec e e)).
     intros.
      rewrite H.
@@ -165,11 +165,11 @@ Module ListDict (E: ELEM).
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
     intros.
-    simpl in |- *.
+    simpl.
     elim (Disequality_provable _ _ _ H (E.eq_dec e e')).
     intros.
      rewrite H0.
-    simpl in |- *.
+    simpl.
     reflexivity.
   Qed.
 
diff --git a/test-suite/modules/errors.v b/test-suite/modules/errors.v
new file mode 100644
index 00000000..d1658786
--- /dev/null
+++ b/test-suite/modules/errors.v
@@ -0,0 +1,70 @@
+(* Inductive mismatches *)
+
+Module Type SA. Inductive TA : nat -> Prop := CA : nat -> TA 0. End SA.
+Module MA : SA. Inductive TA : Prop := CA : bool -> TA. Fail End MA.
+
+Module Type SA. Inductive TA := CA : nat -> TA. End SA.
+Module MA : SA. Inductive TA := CA : bool -> TA. Fail End MA.
+
+Module Type SA. Inductive TA := CA : nat -> TA. End SA.
+Module MA : SA. Inductive TA := CA : bool -> nat -> TA. Fail End MA.
+
+Module Type SA2. Inductive TA2 := CA2 : nat -> TA2. End SA2.
+Module MA2 : SA2. Inductive TA2 := CA2 : nat -> TA2 | DA2 : TA2. Fail End MA2.
+
+Module Type SA3. Inductive TA3 := CA3 : nat -> TA3. End SA3.
+Module MA3 : SA3. Inductive TA3 := CA3 : nat -> TA3 with UA3 := DA3. Fail End MA3.
+
+Module Type SA4. Inductive TA4 := CA4 : nat -> TA4 with UA4 := DA4. End SA4.
+Module MA4 : SA4. Inductive TA4 := CA4 : nat -> TA4 with VA4 := DA4. Fail End MA4.
+
+Module Type SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := DA5. End SA5.
+Module MA5 : SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := EA5. Fail End MA5.
+
+Module Type SA6. Inductive TA6 (A:Type) := CA6 : A -> TA6 A. End SA6.
+Module MA6 : SA6. Inductive TA6 (A B:Type):= CA6 : A -> TA6 A B. Fail End MA6.
+
+Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7.
+Module MA7 : SA7. CoInductive TA7 (A:Type):= CA7 : A -> TA7 A. Fail End MA7.
+
+Module Type SA8. CoInductive TA8 (A:Type) := CA8 : A -> TA8 A. End SA8.
+Module MA8 : SA8. Inductive TA8 (A:Type):= CA8 : A -> TA8 A. Fail End MA8.
+
+Module Type SA9. Record TA9 (A:Type) := { CA9 : A }. End SA9.
+Module MA9 : SA9. Inductive TA9 (A:Type):= CA9 : A -> TA9 A. Fail End MA9.
+
+Module Type SA10. Inductive TA10 (A:Type) := CA10 : A -> TA10 A. End SA10.
+Module MA10 : SA10. Record TA10 (A:Type):= { CA10 : A }. Fail End MA10.
+
+Module Type SA11. Record TA11 (A:Type):= { CA11 : A }. End SA11.
+Module MA11 : SA11. Record TA11 (A:Type):= { DA11 : A }. Fail End MA11.
+
+(* Basic mismatches *)
+Module Type SB. Inductive TB := CB : nat -> TB. End SB.
+Module MB : SB. Module Type TB. End TB. Fail End MB.
+
+Module Type SC. Module Type TC. End TC. End SC.
+Module MC : SC. Inductive TC := CC : nat -> TC. Fail End MC.
+
+Module Type SD. Module TD. End TD. End SD.
+Module MD : SD. Inductive TD := DD : nat -> TD. Fail End MD.
+
+Module Type SE. Definition DE := nat. End SE.
+Module ME : SE. Definition DE := bool. Fail End ME.
+
+Module Type SF. Parameter DF : nat. End SF.
+Module MF : SF. Definition DF := bool. Fail End MF.
+
+(* Needs a type constraint in module type *)
+Module Type SG. Definition DG := Type. End SG.
+Module MG : SG. Definition DG := Type : Type. Fail End MG.
+
+(* Should work *)
+Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7.
+Module MA7 : SA7. Inductive TA7 (B:Type):= CA7 : B -> TA7 B. End MA7.
+
+Module Type SA11. Record TA11 (B:Type):= { CA11 : B }. End SA11.
+Module MA11 : SA11. Record TA11 (A:Type):= { CA11 : A }. End MA11.
+
+Module Type SE. Parameter DE : Type. End SE.
+Module ME : SE. Definition DE := Type : Type. End ME.