aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-02-20 13:55:46 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-02 23:45:51 +0100
commita4817d25befc71b7dbf707637660431144985133 (patch)
treefb0d98df0c5678e5a277ff07de82b43bc8a69b7f /pretyping
parentff7be36add22cf3c6efd24a27ebdde818fc1dc06 (diff)
Remove VOld compatibility flag.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/unification.ml2
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6700748eb..bfc04893d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -923,7 +923,7 @@ 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
+ 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 obj ind p v f =
@@ -1036,7 +1036,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
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
+ 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 csgn =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e1720ec95..48d8a372c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -193,7 +193,7 @@ let pose_all_metas_as_evars env evd t =
let ty = EConstr.of_constr ty 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 || Flags.version_less_or_equal Flags.VOld
+ 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 src = Evd.evar_source_of_meta mv !evdref in