From a4817d25befc71b7dbf707637660431144985133 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Feb 2018 13:55:46 +0100
Subject: Remove VOld compatibility flag.

---
 pretyping/pretyping.ml   | 4 ++--
 pretyping/unification.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6700748ebc..bfc04893d7 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 e1720ec955..48d8a372cf 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
-- 
cgit v1.2.3


From 3ce123f16ce19f67dde4a0f3f2874a2678649907 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Feb 2018 16:03:57 +0100
Subject: Remove 8.5 compatibility support.

---
 pretyping/unification.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 48d8a372cf..6106b6ef63 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1304,12 +1304,7 @@ let solve_simple_evar_eqn ts env evd ev rhs =
   match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (mkEvar ev,rhs);
-  | Success evd ->
-     if Flags.version_less_or_equal Flags.V8_5 then
-       (* We used to force solving unrelated problems at arbitrary times *)
-       Evarconv.solve_unif_constraints_with_heuristics env evd
-     else (* solve_simple_eqn calls reconsider_unif_constraints itself *)
-       evd
+  | Success evd -> evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
-- 
cgit v1.2.3