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/pretyping.ml | |
| 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/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 2 insertions, 7 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 |