diff options
Diffstat (limited to 'test-suite/bugs/closed/4328.v')
| -rw-r--r-- | test-suite/bugs/closed/4328.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v new file mode 100644 index 00000000..8e1bb310 --- /dev/null +++ b/test-suite/bugs/closed/4328.v @@ -0,0 +1,6 @@ +Inductive M (A:Type) : Type := M'. +Axiom pi : forall (P : Prop) (p : P), Prop. +Definition test1 A (x : _) := pi A x. (* success *) +Fail Definition test2 A (x : A) := pi A x. (* failure ??? *) +Fail Definition test3 A (x : A) (_ : M A) := pi A x. (* failure *) +Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *)
\ No newline at end of file |