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 /pretyping/cases.ml | |
| 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 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6bc2a4f94..8a49cd548 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1245,6 +1245,12 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let typs = List.map2 RelDecl.set_name names cs_args in + (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *) + (* This is a bit too strong I think, in the sense that what we would *) + (* really like is to have beta-iota reduction only at the positions where *) + (* parameters are substituted *) + let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in + (* We build the matrix obtained by expanding the matching on *) (* "C x1..xn as x" followed by a residual matching on eqn into *) (* a matching on "x1 .. xn eqn" *) |