aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-25 07:06:46 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-25 07:06:46 +0000
commitc8d991594d9e97e4791dfd9179e6f8290a72ef8b (patch)
treefd5ea6c6276c32a2c22846ebe5e133934ed8856e /theories/Logic
parentf68e8034cd7d146be3dd5fc25b5a897da319655d (diff)
Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création
des schémas d'élimination standard de JMeq, plutôt que "Reset JMeq_rect". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9793 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/JMeq.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 96bab3dc7..a2e156b9f 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -19,9 +19,12 @@
Set Implicit Arguments.
+Unset Elimination Schemes.
+
Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
JMeq_refl : JMeq x x.
-Reset JMeq_rect.
+
+Set Elimination Schemes.
Hint Resolve JMeq_refl.