diff options
| author | Jason Gross | 2018-10-02 14:45:00 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-10-02 14:45:40 -0400 |
| commit | 3208a68e2c1b5f29fe33b54a66a2c361d3bfc531 (patch) | |
| tree | eb3c7d125bed17f2338dc6980a1fac315460ad05 /pretyping | |
| parent | 9e7402632f1aecf5d2dce936d95e296097024ea5 (diff) | |
Update the -compat flags
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
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; |