From 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 28 Apr 2017 16:30:45 +0200 Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... --- test-suite/bugs/closed/5487.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test-suite/bugs/closed/5487.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v new file mode 100644 index 000000000..9b995f450 --- /dev/null +++ b/test-suite/bugs/closed/5487.v @@ -0,0 +1,9 @@ +(* Was a collision between an ltac pattern variable and an evar *) + +Goal forall n, exists m, n = m :> nat. +Proof. + eexists. + Fail match goal with + | [ |- ?x = ?y ] + => match x with y => idtac end + end. -- cgit v1.2.3