diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 17:29:26 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-26 19:47:04 +0200 |
commit | 0658ba7b908dad946200f872f44260d0e4893a94 (patch) | |
tree | df98e761400534d92f47d827d09dda6dc08998c2 /test-suite/success/Case13.v | |
parent | 292f365185b7acdee79f3ff7b158551c2764c548 (diff) |
Posssible abstractions over goal variables when inferring match return clause.
The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".
By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".
See antepenultimate commit for discussion.
Diffstat (limited to 'test-suite/success/Case13.v')
-rw-r--r-- | test-suite/success/Case13.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index 8fad41cd8..356a67efe 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -113,3 +113,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) => | F => f y true H1 | G b => f y b H2 end. + +(* Check use of the maximal-dependency-in-variable strategy for "Var" + variables *) + +Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z. +intros z P Q y H1 H2 f. +Show. +refine (match y with + | F => f y true H1 + | G b => f y b H2 + end). +Qed. |