diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-22 13:50:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-27 17:23:17 +0200 |
| commit | e2a8edaf595827af82be67a90c0c5b22c987abe5 (patch) | |
| tree | ce4018beafe686ecac0d84d07b87aba24d1547f2 /test-suite | |
| parent | 0bfd1f2a461ec989dbe812b10d8ee39d296bc777 (diff) | |
A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".
There is a long story of commits trying to improve the compatibility
between 8.4 and 8.5 refine, as discussed in
https://github.com/coq/coq/pull/346.
ac9c5986b77bf4a783f2bd0ad571645694c960e1 add beta-iota in hypotheses and conclusion
8afac4f87d9d7e3add1c19485f475bd2207bfde7 remove beta-iota in hypotheses
08e87eb96ab67ead60d92394eec6066d9b52e55e re-add beta-iota in hypotheses
c9c54122d1d9493a965b483939e119d52121d5a6 re-remove beta-iota in hypotheses
9194180e2da0f7f9a2b2c7574bb7261cc69ead17 revert re-remove beta-iota in hypotheses
6bb352a6743c7332b9715ac15e95c806a58d101c re-re-remove beta-iota in hypotheses if <= 8.5
d8baa76d86eaa691a5386669596a6004bb44bb7a idem if = 8.5
The current commit tries to identify (one of?) the exact points of
divergence between 8.4 and 8.5 refine, namely the types inferred for
the variables of a pattern-matching problem.
Note that for the conclusion of each new goal, there were a
nf_betaiota in 8.4 done in function Evarutil.evars_to_metas, so the
compatibility expects that such a nf_betaiota on the conclusion of
each goal remains.
Diffstat (limited to 'test-suite')
0 files changed, 0 insertions, 0 deletions