diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 9 | ||||
| -rw-r--r-- | pretyping/unification.ml | 5 |
2 files changed, 3 insertions, 11 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 162adf0626..d86c094b1f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -795,9 +795,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in - let fsign = if Flags.version_strictly_greater Flags.V8_6 - then Context.Rel.map (whd_betaiota !evdref) fsign - else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in + let fsign = Context.Rel.map (whd_betaiota !evdref) fsign in let fsign,env_f = push_rel_context !evdref fsign env in let obj ind p v f = if not record then @@ -896,10 +894,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref 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 - then Context.Rel.map (whd_betaiota !evdref) cs_args - else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in + let cs_args = Context.Rel.map (whd_betaiota !evdref) cs_args in let csgn = List.map (set_name Anonymous) cs_args in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e223674579..4665486fc0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -193,10 +193,7 @@ let pose_all_metas_as_evars env evd t = | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in - let ty = - if Flags.version_strictly_greater Flags.V8_6 - then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) - else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in + let ty = nf_betaiota env evd ty in let src = Evd.evar_source_of_meta mv !evdref in let evd, ev = Evarutil.new_evar env !evdref ~src ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd; |