diff options
| author | Hugo Herbelin | 2017-07-26 22:34:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-21 13:14:43 +0200 |
| commit | dd56ef10395a2ced84612aa799690b034306806e (patch) | |
| tree | e6fe2bc49b5154c5f6ee8f951a900905f4260af0 | |
| parent | 9490c6099e1da94fcf315aba48125993cd180327 (diff) | |
Fixing another regression with 8.4 wrt to βι-normalization of created hyps.
This one is a continuation of e2a8edaf59 which was βι-normalizing the
hypotheses created by a "match". We forgot to do it for "let" and
"if". This is what this commit is doing.
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | test-suite/success/refine.v | 10 |
2 files changed, 17 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b4d87dfdb0..a292986bcd 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -904,6 +904,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in + let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) fsign + else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in @@ -1017,6 +1020,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in + let cs_args = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) cs_args + else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs_args diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 352abb2af5..4f6505f583 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -122,3 +122,13 @@ Abort. Goal (forall A : Prop, A -> ~~A). Proof. refine(fun A a f => _). + +(* Checking beta-iota normalization of hypotheses in created evars *) + +Goal {x|x=0} -> True. +refine (fun y => let (x,a) := y in _). +match goal with a:_=0 |- _ => idtac end. + +Goal (forall P, {P 0}+{P 1}) -> True. +refine (fun H => if H (fun x => x=x) then _ else _). +match goal with _:0=0 |- _ => idtac end. |