diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:20:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:23:49 +0200 |
| commit | db28e827d21658797418c320d566fb99570b44b6 (patch) | |
| tree | a4fd54fedd13150bd30cedd1778634bb2344af9b /test-suite | |
| parent | 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d (diff) | |
Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."
One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:
~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~
Thank you!
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5487.v | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v deleted file mode 100644 index 9b995f450..000000000 --- a/test-suite/bugs/closed/5487.v +++ /dev/null @@ -1,9 +0,0 @@ -(* 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. |