remplacement d'un test d'egalite par un test de convertibilite dans injection/discriminate/inversion pour corriger des bugs en presence de modules.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7

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 000000000..88c19cb1a
--- /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