From e2a8edaf595827af82be67a90c0c5b22c987abe5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 22 Nov 2016 13:50:10 +0100 Subject: 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. --- pretyping/cases.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'pretyping/cases.ml') 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" *) -- cgit v1.2.3