diff options
author | 2017-04-15 22:51:20 +0200 | |
---|---|---|
committer | 2017-04-20 15:39:53 +0200 | |
commit | 1fb4d1ef961f056e3575c5e034cace85f2340509 (patch) | |
tree | 1ee7b34b2f30d9076c304476b532a1c4ac86060a /test-suite | |
parent | 59b0041147a9d2dddc1fe14f624a2cf5695f2ea2 (diff) |
Fix bug #5377: @? patterns broken.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/5377.v | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5377.v b/test-suite/bugs/closed/5377.v new file mode 100644 index 000000000..130d9f9ab --- /dev/null +++ b/test-suite/bugs/closed/5377.v @@ -0,0 +1,54 @@ +Goal ((forall (t : Type) (x y : t), + True -> + x = y)) -> False. +Proof. + intro HG. + let P := lazymatch goal with + | [ H : forall t x y, True -> @?P t x y + |- _ ] + => P + end in + pose (f := P). + unify f (fun (t : Type) (x y : t) => x = y). +Abort. + +Goal True. +Proof. +let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with + | fun _ y _ => @?C y => C + end in +pose (f := c). +unify f (fun n : nat => n). +Abort. + +Goal (forall x : nat, x = x -> x = x \/ x = x) -> True. +Proof. +intro. +let P := lazymatch goal with +| [ H : forall y, @?P y -> @?P y \/ _ |- _ ] + => P +end in +pose (f := P). +unify f (fun x : nat => x = x). +Abort. + +Goal (forall x : nat, x = x -> x = x \/ x = x) -> True. +Proof. +intro. +lazymatch goal with +| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ] + => idtac +end. +Abort. + +Axiom eq : forall {T} (_ : T), Prop. + +Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop. +Proof. +intro. +let P := lazymatch goal with +| [ H : forall t _ x, @?P t x |- _ ] + => P +end in +pose (f := P). +Abort. |