diff options
| author | Hugo Herbelin | 2014-11-03 19:31:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-02 22:39:22 +0100 |
| commit | e2fa65fccb9d55ea0b6bd5873155abf436785b1f (patch) | |
| tree | 92f016008068f618703362818a4b4428729c968b /test-suite/success | |
| parent | 6fd7634319e7a82e89667d3fc70ecbd65e7bf45c (diff) | |
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
possible, which is the "natural" way to orient an equation. At least
it matters for matching subterms against patterns, so that it is the
pattern variables which are substituted if ever the subterm has itself
existential variables, as in:
Goal exists x, S x = x.
eexists.
destruct (S _).
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/destruct.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 277e3ca60a..d3aca59a2a 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -420,4 +420,11 @@ Abort. Goal forall b:bool, b = b. intros. destruct b eqn:H. + +(* Check natural instantiation behavior when the goal has already an evar *) + +Goal exists x, S x = x. +eexists. +destruct (S _). +change (0 = ?x). Abort. |