From 6986bb7e16523c62776628558a9ec8e7c6b028a7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 28 Oct 2019 16:16:34 +0100
Subject: [abstract] Remove un-unused reference to `evar_map`

We use an `evar_map ref` even tho the modification the `evar_map` is
ignored.

I'm not sure if this is a bug or not, so I am making thus preserving
the behavior but making the what is going with the `evar_map` more
explicit.
---
 tactics/abstract.ml | 37 +++++++++++++++++++------------------
 1 file changed, 19 insertions(+), 18 deletions(-)

(limited to 'tactics')

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 03ab0a1c13..9b4a628871 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -23,19 +23,21 @@ module NamedDecl = Context.Named.Declaration
    is solved by tac *)
 
 (** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl env evd d1 d2 =
+let interpretable_as_section_decl env sigma d1 d2 =
   let open Context.Named.Declaration in
-  let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with
-  | None -> false
-  | Some cstr ->
-    try ignore (Evd.add_universe_constraints !sigma cstr); true
-    with UState.UniversesDiffer -> false
+  let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env sigma c1 c2 with
+    | None -> false
+    | Some cstr ->
+      try
+        let _sigma = Evd.add_universe_constraints sigma cstr in
+        true
+      with UState.UniversesDiffer -> false
   in
   match d2, d1 with
   | LocalDef _, LocalAssum _ -> false
   | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
-    e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
-  | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
+    e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2
+  | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma t1 (NamedDecl.get_type d2)
 
 let rec decompose len c t accu =
   let open Constr in
@@ -110,13 +112,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let sigma = Proofview.Goal.sigma gl in
   let current_sign = Global.named_context_val ()
   and global_sign = Proofview.Goal.hyps gl in
-  let evdref = ref sigma in
   let sign,secsign =
     List.fold_right
       (fun d (s1,s2) ->
         let id = NamedDecl.get_id d in
         if mem_named_context_val id current_sign &&
-          interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d
+          interpretable_as_section_decl env sigma (lookup_named_val id current_sign) d
         then (s1,push_named_context_val d s2)
         else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, Environ.empty_named_context_val) in
@@ -126,19 +127,19 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
               | Some ty -> ty in
   let concl = it_mkNamedProd_or_LetIn concl sign in
   let concl =
-    try flush_and_check_evars !evdref concl
+    try flush_and_check_evars sigma concl
     with Uninstantiated_evar _ ->
       CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in
 
-  let evd, ctx, concl =
+  let sigma, ctx, concl =
     (* FIXME: should be done only if the tactic succeeds *)
-    let evd = Evd.minimize_universes !evdref in
-    let ctx = Evd.universe_context_set evd in
-      evd, ctx, Evarutil.nf_evars_universes evd concl
+    let sigma = Evd.minimize_universes sigma in
+    let ctx = Evd.universe_context_set sigma in
+    sigma, ctx, Evarutil.nf_evars_universes sigma concl
   in
   let concl = EConstr.of_constr concl in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
-  let ectx = Evd.evar_universe_context evd in
+  let ectx = Evd.evar_universe_context sigma in
   let (const, safe, ectx) =
     try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
@@ -174,14 +175,14 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     EInstance.make (Univ.UContext.instance ctx)
   in
   let lem = mkConstU (cst, inst) in
-  let evd = Evd.set_universe_context evd ectx in
+  let sigma = Evd.set_universe_context sigma ectx in
   let effs = Evd.concat_side_effects eff effs in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
-  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
   end
 
 let abstract_subproof ~opaque tac =
-- 
cgit v1.2.3