diff options
| author | Matthieu Sozeau | 2015-09-23 18:53:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:11 +0200 |
| commit | 91e01278de2420a64f1c8de03c0bc6e614577042 (patch) | |
| tree | 759e189e430076511069e272901550aa96ec93b7 | |
| parent | 91b1808056602f3e26d1eb1bdf7be1e791cb742d (diff) | |
Univs: fixed bug #4328.
| -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 0000000000..8e1bb31007 --- /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 |