Merge PR #7359: Reduce usage of evar_map references

3 files changed, 42 insertions, 41 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c542d..2408b8f2b2 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -70,11 +70,10 @@ let first_goal gls =
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
 
 let apply_tac_list tac glls =
-  let (sigr,lg) = unpackage glls in
-  match lg with
+  match glls.it with
   | (g1::rest) ->
-      let gl = apply_sig_tac sigr tac g1 in
-      repackage sigr (gl@rest)
+      let pack = tac (re_sig g1 glls.sigma) in
+      re_sig (pack.it @ rest) pack.sigma
   | _ -> user_err Pp.(str "apply_tac_list")
 
 let one_step l gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b6bbd0be45..d142e10a4f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1176,34 +1176,35 @@ let minimal_free_rels_rec env sigma =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let sigdata = find_sigma_data env sort_of_ty in
-  let evdref = ref (Evd.clear_metas sigma) in
-  let rec sigrec_clausal_form siglen p_i =
+  let rec sigrec_clausal_form sigma siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
-	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
-	let () =
-          evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
-	dflt
+        let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
+        let sigma =
+          Evarconv.solve_unif_constraints_with_heuristics env sigma in
+        sigma, dflt
       with Evarconv.UnableToUnify _ ->
 	user_err Pp.(str "Cannot solve a unification problem.")
     else
-      let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
 	| (_sigS,[a;p]) -> (a, p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
-      let ev = Evarutil.e_new_evar env evdref a in
+      let sigma, ev = Evarutil.new_evar env sigma a in
       let rty = beta_applist sigma (p_i_minus_1,[ev]) in
-      let tuple_tail = sigrec_clausal_form (siglen-1) rty in
-      let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
+      let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
+      let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
       match evopt with
 	| Some w ->
-            let w_type = unsafe_type_of env !evdref w in
-            if Evarconv.e_cumul env evdref w_type a then
-	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
-              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
-            else
+          let w_type = unsafe_type_of env sigma w in
+          begin match Evarconv.cumul env sigma w_type a with
+            | Some sigma ->
+              let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
+              sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+            | None ->
               user_err Pp.(str "Cannot solve a unification problem.")
+          end
 	| None ->
             (* This at least happens if what has been detected as a
                dependency is not one; use an evasive error message;
@@ -1213,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
                unsolved evars would mean not binding rel *)
 	    user_err Pp.(str "Cannot solve a unification problem.")
   in
-  let scf = sigrec_clausal_form siglen ty in
-    !evdref, Evarutil.nf_evar !evdref scf
+  let sigma = Evd.clear_metas sigma in
+  let sigma, scf = sigrec_clausal_form sigma siglen ty in
+    sigma, Evarutil.nf_evar sigma scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ee76ad077a..01351e2492 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -247,13 +247,12 @@ let clear_gen fail = function
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
-    let evdref = ref sigma in
-    let (hyps, concl) =
-      try clear_hyps_in_evi env evdref (named_context_val env) concl ids
+    let (sigma, hyps, concl) =
+      try clear_hyps_in_evi env sigma (named_context_val env) concl ids
       with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
     in
     let env = reset_with_named_context hyps env in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Refine.refine ~typecheck:false begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
     end)
@@ -431,9 +430,8 @@ let get_previous_hyp_position env sigma id =
 
 let clear_hyps2 env sigma ids sign t cl =
   try
-    let evdref = ref (Evd.clear_metas sigma) in
-    let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
-    (hyps, t, cl, !evdref)
+    let sigma = Evd.clear_metas sigma in
+    Evarutil.clear_hyps2_in_evi env sigma sign t cl ids
   with Evarutil.ClearDependencyError (id,err,inglobal) ->
     error_replacing_dependency env sigma id err inglobal
 
@@ -447,7 +445,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
     let sign',t,concl,sigma =
       if replace then
         let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
-        let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
+        let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
         let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
         sign',t,concl,sigma
       else
@@ -1987,24 +1985,22 @@ let on_the_bodies = function
 exception DependsOnBody of Id.t option
 
 let check_is_type env sigma ty =
-  let evdref = ref sigma in
   try
-    let _ = Typing.e_sort_of env evdref ty in
-    !evdref
+    let sigma, _ = Typing.sort_of env sigma ty in
+    sigma
   with e when CErrors.noncritical e ->
     raise (DependsOnBody None)
 
 let check_decl env sigma decl =
   let open Context.Named.Declaration in
   let ty = NamedDecl.get_type decl in
-  let evdref = ref sigma in
   try
-    let _ = Typing.e_sort_of env evdref ty in
-    let _ = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
+    let sigma, _ = Typing.sort_of env sigma ty in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,c,_) -> Typing.check env sigma c ty
     in
-    !evdref
+    sigma
   with e when CErrors.noncritical e ->
     let id = NamedDecl.get_id decl in
     raise (DependsOnBody (Some id))
@@ -3815,7 +3811,10 @@ let specialize_eqs id =
   let ty = Tacmach.New.pf_get_hyp_typ id gl in
   let evars = ref (Proofview.Goal.sigma gl) in
   let unif env evars c1 c2 =
-    compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
+    compare_upto_variables !evars c1 c2 &&
+    (match Evarconv.conv env !evars c1 c2 with
+     | Some sigma -> evars := sigma; true
+     | None -> false)
   in
   let rec aux in_eqs ctx acc ty =
     match EConstr.kind !evars ty with
@@ -3840,7 +3839,8 @@ let specialize_eqs id =
 	| _ ->
 	    if in_eqs then acc, in_eqs, ctx, ty
 	    else
-	      let e = e_new_evar (push_rel_context ctx env) evars t in
+              let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
+              evars := sigma;
 		aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
     | t -> acc, in_eqs, ctx, ty
   in
@@ -4367,7 +4367,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
   let (_,u,_) = destProd sigma cl.cl_concl in
-  fun t -> Evarconv.e_cumul env (ref sigma) t u
+  fun t -> Option.has_some (Evarconv.cumul env sigma t u)
 
 let check_enough_applied env sigma elim =
   (* A heuristic to decide whether the induction arg is enough applied *)