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 /theories/Vectors | |
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 'theories/Vectors')
0 files changed, 0 insertions, 0 deletions