diff options
| author | Maxime Dénès | 2017-05-11 13:45:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-11 13:45:23 +0200 |
| commit | b75d7f21a49bb7c2b7684a06ad3fae89b99e7a94 (patch) | |
| tree | 0178bb45ed3fbef92f9aca887ea536ff497e2686 | |
| 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"
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | pretyping/cases.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5219.v | 10 |
3 files changed, 21 insertions, 0 deletions
@@ -18,6 +18,11 @@ Tactics missed before because of a missing normalization step. Hopefully this should be fairly uncommon. - "auto with real" can now discharge comparisons of literals +- The types of variables in patterns of "match" are now + beta-iota-reduced after type-checking. This has an impact on the + type of the variables that the tactic "refine" introduces in the + context, producing types a priori closer to the expectations. + Standard Library diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6bc2a4f94b..8a49cd5488 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" *) diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v new file mode 100644 index 0000000000..f7cec1a0cf --- /dev/null +++ b/test-suite/bugs/closed/5219.v @@ -0,0 +1,10 @@ +(* Test surgical use of beta-iota in the type of variables coming from + pattern-matching for refine *) + +Goal forall x : sigT (fun x => x = 1), True. + intro x; refine match x with + | existT _ x' e' => _ + end. + lazymatch goal with + | [ H : _ = _ |- _ ] => idtac + end. |