From c8d991594d9e97e4791dfd9179e6f8290a72ef8b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 25 Apr 2007 07:06:46 +0000
Subject: 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
---
 theories/Logic/JMeq.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 96bab3dc7b..a2e156b9ff 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.
 
-- 
cgit v1.2.3