diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:45:23 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:45:23 +0200 |
| commit | b75d7f21a49bb7c2b7684a06ad3fae89b99e7a94 (patch) | |
| tree | 0178bb45ed3fbef92f9aca887ea536ff497e2686 /pretyping | |
| parent | e176622f715772cc0704dc860ffa18e85c36e250 (diff) | |
| parent | cc1212c3cfbd9c39cbe981210758c67cf9095be2 (diff) | |
Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 and 8.5/8.6 "refine"
Diffstat (limited to 'pretyping')
| -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" *) |