1 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v
new file mode 100644
index 00000000..88c19cb1
--- /dev/null
+++ b/test-suite/modules/injection_discriminate_inversion.v
@@ -0,0 +1,34 @@
+Module M.
+  Inductive I : Set := C : nat -> I.
+End M.
+
+Module M1 := M.
+
+
+Goal forall x, M.C x = M1.C 0 -> x = 0 .
+  intros x H.
+  (* 
+     injection sur deux constructeurs egaux mais appeles 
+     par des modules differents 
+     *)
+  injection H. 
+  tauto.
+Qed.
+
+Goal  M.C 0 <> M1.C 1.
+  (* 
+     Discriminate sur deux constructeurs egaux mais appeles 
+     par des modules differents 
+     *)
+  intro H;discriminate H.
+Qed.
+
+
+Goal forall x,  M.C x = M1.C 0 -> x = 0.
+  intros x H.
+  (* 
+     inversion sur deux constructeurs egaux mais appeles 
+     par des modules differents 
+     *)
+  inversion H. reflexivity.
+Qed.
+\ No newline at end of file