blob: c4dbf74cd2dec8b7cddcbd809f29beeaa89110ab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(** JMeq should be polymorphic *)
Require Import JMeq.
Set Implicit Arguments.
Monomorphic Inductive JMeq' (A : Type) (x : A)
: forall B : Type, B -> Prop :=
JMeq'_refl : JMeq' x x.
Fail Monomorphic Definition foo := @JMeq' _ (@JMeq').
Monomorphic Definition bar := @JMeq _ (@JMeq).
|
