diff options
| author | Théo Zimmermann | 2018-10-03 13:03:12 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-03 13:03:12 +0200 |
| commit | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (patch) | |
| tree | adb720db54d759a3c722a8c57de6eaca0ddbd228 /pretyping | |
| parent | 33328635560b9cb963af0805c43f170b3898caac (diff) | |
| parent | 425475e4605691642b09b625dd13e7e3506299b6 (diff) | |
Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the compat updates to do as part of a release.
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 a40c0d2375..1b7f32bcae 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -790,9 +790,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 @@ -891,10 +889,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; |