diff options
| -rw-r--r-- | theories/Logic/JMeq.v | 5 |
1 files changed, 4 insertions, 1 deletions
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. |