From 864fda19d046428023851ba540b82c5ca24d06a4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 25 Apr 2018 18:08:39 +0200
Subject: Deprecate most evarutil evdref functions

clear_hyps remain with no alternative
---
 engine/evarutil.mli            | 38 +++++++++++++++++-------------
 plugins/setoid_ring/newring.ml | 53 +++++++++++++++++++++++-------------------
 pretyping/cases.ml             | 18 +++++++++-----
 pretyping/coercion.ml          |  4 +++-
 pretyping/evarconv.ml          | 10 ++++++++
 pretyping/evarconv.mli         |  3 +++
 pretyping/program.ml           |  4 +++-
 pretyping/unification.ml       |  4 ++--
 tactics/equality.ml            | 36 ++++++++++++++--------------
 tactics/tactics.ml             |  3 ++-
 10 files changed, 105 insertions(+), 68 deletions(-)

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 3bbd2923c..7595de04c 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -50,13 +50,6 @@ val new_pure_evar :
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
 
-(** the same with side-effects *)
-val e_new_evar :
-  env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> ?hypnaming:naming_mode -> types -> constr
-
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
@@ -65,13 +58,7 @@ val new_type_evar :
   ?principal:bool -> ?hypnaming:naming_mode -> rigid ->
   evar_map * (constr * Sorts.t)
 
-val e_new_type_evar : env -> evar_map ref ->
-  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
-
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
 val restrict_evar : evar_map -> Evar.t -> Filter.t ->
   ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
@@ -79,7 +66,6 @@ val restrict_evar : evar_map -> Evar.t -> Filter.t ->
 (** Polymorphic constants *)
 
 val new_global : evar_map -> GlobRef.t -> evar_map * constr
-val e_new_global : evar_map ref -> GlobRef.t -> constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -187,8 +173,6 @@ val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
 
 val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
 [@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
-val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
-[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
 
 (** Normalize the evar map w.r.t. universes, after simplification of constraints.
     Return the substitution function for constrs as well. *)
@@ -276,3 +260,25 @@ type type_constraint = types option
 [@@ocaml.deprecated "use the version in Evardefine"]
 type val_constraint = constr option
 [@@ocaml.deprecated "use the version in Evardefine"]
+
+val e_new_evar :
+  env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> ?hypnaming:naming_mode -> types -> constr
+[@@ocaml.deprecated "Use [Evd.new_evar]"]
+
+val e_new_type_evar : env -> evar_map ref ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
+[@@ocaml.deprecated "Use [Evd.new_type_evar]"]
+
+val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
+[@@ocaml.deprecated "Use [Evd.new_Type]"]
+
+val e_new_global : evar_map ref -> GlobRef.t -> constr
+[@@ocaml.deprecated "Use [Evd.new_global]"]
+
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 5facf2a80..b2ac3b5a4 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -247,9 +247,10 @@ let coq_nil = coq_reference "nil"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
-let plapp evd f args = 
-  let fc = Evarutil.e_new_global evd (Lazy.force f) in
-    mkApp(fc,args)
+let plapp evdref f args =
+  let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
+  evdref := evd;
+  mkApp(fc,args)
 
 let dest_rel0 sigma t =
   match EConstr.kind sigma t with
@@ -586,48 +587,52 @@ let make_hyp env evd c =
   let t = Retyping.get_type_of env !evd c in
    plapp evd coq_mkhypo [|t;c|]
 
-let make_hyp_list env evd lH =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let make_hyp_list env evdref lH =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   let l = 
     List.fold_right
-      (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
-      (plapp evd coq_nil [|carrier|])
+      (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
+      (plapp evdref coq_nil [|carrier|])
   in 
-  let l' = Typing.e_solve_evars env evd l in
+  let l' = Typing.e_solve_evars env evdref l in
   let l' = EConstr.Unsafe.to_constr l' in
-    Evarutil.nf_evars_universes !evd l'
+    Evarutil.nf_evars_universes !evdref l'
 
-let interp_power env evd pow =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_power env evdref pow =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   match pow with
   | None ->
       let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
-      (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|])
+      (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
         | CstTac t -> Tacintern.glob_tactic t
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
-      let spec = make_hyp env evd (ic_unsafe spec) in
-      (tac, plapp evd coq_Some [|carrier; spec|])
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      (tac, plapp evdref coq_Some [|carrier; spec|])
 
-let interp_sign env evd sign =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_sign env evdref sign =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   match sign with
-  | None -> plapp evd coq_None [|carrier|]
+  | None -> plapp evdref coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env evd (ic_unsafe spec) in
-      plapp evd coq_Some [|carrier;spec|]
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      plapp evdref coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let interp_div env evd div =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_div env evdref div =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   match div with
-  | None -> plapp evd coq_None [|carrier|]
+  | None -> plapp evdref coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env evd (ic_unsafe spec) in
-      plapp evd coq_Some [|carrier;spec|]
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      plapp evdref coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
 let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4c87b4e7e..16244d8c0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -295,7 +295,8 @@ let inductive_template evdref env tmloc ind =
         | LocalAssum (na,ty) ->
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
-	    let e = e_new_evar env evdref ~src:(hole_source n) ty' in
+            let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in
+            evdref := evd;
 	    (e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
             let b = EConstr.of_constr b in
@@ -396,7 +397,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
-  let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
+  let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in
+  evdref := evd;
+  e
 
 let evd_comb2 f evdref x y =
   let (evd',y) = f !evdref x y in
@@ -1681,7 +1684,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ev' = e_new_evar env evdref ~src ty in
+        let evd, ev' = Evarutil.new_evar env !evdref ~src ty in
+        evdref := evd;
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1712,7 +1716,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	  (named_context extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
-      let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
+      let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in
+      evdref := evd;
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1724,8 +1729,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
            we are in an impossible branch *)
 	let n = Context.Rel.length (rel_context env) in
 	let n' = Context.Rel.length (rel_context tycon_env) in
-	let impossible_case_type, u =
-	  e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
+        let evd, (impossible_case_type, u) =
+          new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
+        evdref := evd;
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6dc3687a0..e8b17d694 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -94,7 +94,9 @@ open Program
 
 let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
   let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
-  Evarutil.e_new_evar env evdref ~src c
+  let evd, v = Evarutil.new_evar env !evdref ~src c in
+  evdref := evd;
+  v
 
 let app_opt env evdref f t =
   whd_betaiota !evdref (app_opt f t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 144166a34..2144639d5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1394,6 +1394,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
+let make_opt = function
+  | Success evd -> Some evd
+  | UnifFailure _ -> None
+
+let conv env ?(ts=default_transparent_state env) evd t1 t2 =
+  make_opt(evar_conv_x ts env evd CONV t1 t2)
+
+let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
+  make_opt(evar_conv_x ts env evd CUMUL t1 t2)
+
 let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
   match evar_conv_x ts env !evdref CONV t1 t2 with
   | Success evd' -> evdref := evd'; true
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9270d6e3a..da2b4d1b8 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -30,6 +30,9 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
 val e_conv  : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
 val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
 
+val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+
 (** {6 Unification heuristics. } *)
 
 (** Try heuristics to solve pending unification problems and to solve
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 52d940d8e..8cfb7966c 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -16,7 +16,9 @@ let init_reference dir s () = Coqlib.coq_reference  "Program" dir s
 let papp evdref r args = 
   let open EConstr in
   let gr = delayed_force r in
-    mkApp (Evarutil.e_new_global evdref gr, args)
+  let evd, hd = Evarutil.new_global !evdref gr in
+  evdref := evd;
+  mkApp (hd, args)
 
 let sig_typ = init_reference ["Init"; "Specif"] "sig"
 let sig_intro = init_reference ["Init"; "Specif"] "exist"
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d98ce9aba..1caa629ff 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t =
           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
-        let ev = Evarutil.e_new_evar env evdref ~src ty in
-        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
+        let evd, ev = Evarutil.new_evar env !evdref ~src ty in
+        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
         ev)
   | _ ->
       EConstr.map !evdref aux t in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b6bbd0be4..d142e10a4 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 ee76ad077..178c10815 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3840,7 +3840,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
-- 
cgit v1.2.3


From c538b7fd555828d9fba9ea97503fac6c70377b76 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 25 Apr 2018 18:12:41 +0200
Subject: Convert clear_hyps_in_evi to state passing style.

---
 engine/evarutil.ml                  | 17 +++++++++--------
 engine/evarutil.mli                 |  8 ++++----
 plugins/ssrmatching/ssrmatching.ml4 |  7 +++----
 tactics/tactics.ml                  | 14 ++++++--------
 4 files changed, 22 insertions(+), 24 deletions(-)

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6c27d5937..52610f6f3 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -613,10 +613,11 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 
       | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c
 
-let clear_hyps_in_evi_main env evdref hyps terms ids =
+let clear_hyps_in_evi_main env sigma hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occurring in evi *)
+  let evdref = ref sigma in
   let terms = List.map EConstr.Unsafe.to_constr terms in
   let global = Id.Set.exists is_section_variable ids in
   let terms =
@@ -639,16 +640,16 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
     in
       remove_hyps ids check_context check_value hyps
   in
-  (nhyps,List.map EConstr.of_constr terms)
+  (!evdref, nhyps,List.map EConstr.of_constr terms)
 
-let clear_hyps_in_evi env evdref hyps concl ids =
-  match clear_hyps_in_evi_main env evdref hyps [concl] ids with
-  | (nhyps,[nconcl]) -> (nhyps,nconcl)
+let clear_hyps_in_evi env sigma hyps concl ids =
+  match clear_hyps_in_evi_main env sigma hyps [concl] ids with
+  | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl)
   | _ -> assert false
 
-let clear_hyps2_in_evi env evdref hyps t concl ids =
-  match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
-  | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
+let clear_hyps2_in_evi env sigma hyps t concl ids =
+  match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with
+  | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl)
   | _ -> assert false
 
 (* spiwack: a few functions to gather evars on which goals depend. *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 7595de04c..c24660f5b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -221,11 +221,11 @@ type clear_dependency_error =
 
 exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option
 
-val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
-  Id.Set.t -> named_context_val * types
+val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types ->
+  Id.Set.t -> evar_map * named_context_val * types
 
-val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
-  Id.Set.t -> named_context_val * types * types
+val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types ->
+  Id.Set.t -> evar_map * named_context_val * types * types
 
 type csubst
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a10437a63..0dd3625ba 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1099,15 +1099,14 @@ let thin id sigma goal =
   let ids = Id.Set.singleton id in
   let env = Goal.V82.env sigma goal in
   let cl = Goal.V82.concl sigma goal in
-  let evdref = ref (Evd.clear_metas sigma) in
+  let sigma = Evd.clear_metas sigma in
   let ans =
-    try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids)
+    try Some (Evarutil.clear_hyps_in_evi env sigma (Environ.named_context_val env) cl ids)
     with Evarutil.ClearDependencyError _ -> None
   in
   match ans with
   | None -> sigma
-  | Some (hyps, concl) ->
-    let sigma = !evdref in
+  | Some (sigma, hyps, concl) ->
     let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
     let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
     sigma
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 178c10815..66505edb5 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
-- 
cgit v1.2.3


From 81107b12644c78f204d0a46df520b8b2d8e72142 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:25:30 +0200
Subject: Deprecate Evarconv.e_conv,e_cumul

---
 plugins/funind/functional_principles_proofs.ml |  2 +-
 pretyping/cases.ml                             | 15 +++---
 pretyping/coercion.ml                          | 32 ++++++-----
 pretyping/evarconv.mli                         |  3 ++
 pretyping/pretyping.ml                         | 27 ++++++----
 pretyping/typing.ml                            | 75 +++++++++++++++-----------
 pretyping/typing.mli                           |  4 +-
 tactics/tactics.ml                             |  7 ++-
 8 files changed, 101 insertions(+), 64 deletions(-)

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da0e1c4f..a0616b308 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -243,7 +243,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       raise NoChange;
     end
   in
-  let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in
+  let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
   if not (noccurn sigma 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp sigma t) then nochange "not an equality";
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 16244d8c0..84f0aba8c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -315,13 +315,15 @@ let try_find_ind env sigma typ realnames =
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind evdref env loc ty tyi =
-  let sigma = !evdref in
+  let orig = !evdref in
   let expected_typ = inductive_template evdref env loc tyi in
   (* Try to refine the type with inductive information coming from the
      constructor and renounce if not able to give more information *)
   (* devrait être indifférent d'exiger leq ou pas puisque pour
      un inductif cela doit être égal *)
-  if not (e_cumul env evdref expected_typ ty) then evdref := sigma
+  match cumul env !evdref expected_typ ty with
+  | Some sigma -> evdref := sigma
+  | None -> evdref := orig
 
 let binding_vars_of_inductive sigma = function
   | NotInd _ -> []
@@ -427,7 +429,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 	    let current =
 	      if List.is_empty deps && isEvar !(pb.evdref) typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-		let _ = e_cumul pb.env pb.evdref indt typ in
+                let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to true pb.env)
@@ -1738,9 +1740,10 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
         let evd,tt = Typing.type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
-  let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
-  if not b then anomaly (Pp.str "Build_tycon: should be a type.");
-  { uj_val = t; uj_type = tt }
+  match cumul env !evdref tt (mkSort s) with
+  | None -> anomaly (Pp.str "Build_tycon: should be a type.");
+  | Some sigma -> evdref := sigma;
+    { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e8b17d694..ea8557b18 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -48,31 +48,35 @@ exception NoCoercion
 exception NoCoercionNoUnifier of evar_map * unification_error
 
 (* Here, funj is a coercion therefore already typed in global context *)
-let apply_coercion_args env evd check isproj argl funj =
-  let evdref = ref evd in
-  let rec apply_rec acc typ = function
+let apply_coercion_args env sigma check isproj argl funj =
+  let rec apply_rec sigma acc typ = function
     | [] ->
       if isproj then
-	let cst = fst (destConst !evdref (j_val funj)) in
+        let cst = fst (destConst sigma (j_val funj)) in
 	let p = Projection.make cst false in
 	let pb = lookup_projection p env in
 	let args = List.skipn pb.Declarations.proj_npars argl in
 	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
-	  { uj_val = applist (mkProj (p, hd), tl);
-	    uj_type = typ }
+        sigma, { uj_val = applist (mkProj (p, hd), tl);
+                 uj_type = typ }
       else
-	{ uj_val = applist (j_val funj,argl);
-	  uj_type = typ }
+        sigma, { uj_val = applist (j_val funj,argl);
+                 uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
-      match EConstr.kind !evdref (whd_all env !evdref typ) with
+      match EConstr.kind sigma (whd_all env sigma typ) with
       | Prod (_,c1,c2) ->
-        if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then
-	  raise NoCoercion;
-        apply_rec (h::acc) (subst1 h c2) restl
+        let sigma =
+          if check then
+            begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with
+              | None -> raise NoCoercion
+              | Some sigma -> sigma
+            end
+          else sigma
+        in
+        apply_rec sigma (h::acc) (subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args.")
   in
-  let res = apply_rec [] funj.uj_type argl in
-    !evdref, res
+  apply_rec sigma [] funj.uj_type argl
 
 (* appliquer le chemin de coercions de patterns p *)
 let apply_pattern_coercion ?loc pat p =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index da2b4d1b8..bea3eeb2e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -28,7 +28,10 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
 (** The same function resolving evars by side-effect and
    catching the exception *)
 val e_conv  : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
+[@@ocaml.deprecated "Use [Evarconv.conv]"]
+
 val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
+[@@ocaml.deprecated "Use [Evarconv.cumul]"]
 
 val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
 val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e68a25a87..35cc5702a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -674,14 +674,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
     let nbfix = Array.length lar in
     let names = Array.map (fun id -> Name id) names in
-    let _ = 
+    let () =
       match tycon with
       | Some t -> 
  	let fixi = match fixkind with
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
-	in e_conv env.ExtraEnv.env evdref ftys.(fixi) t
-      | None -> true
+        in
+        begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with
+          | None -> ()
+          | Some sigma -> evdref := sigma
+        end
+      | None -> ()
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
     let newenv = push_rec_types !evdref (names,ftys,[||]) env in
@@ -698,7 +702,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj;
+      evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj;
       let nf c = nf_evar !evdref c in
       let ftys = Array.map nf ftys in (** FIXME *)
       let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
@@ -793,9 +797,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      match candargs with
 	      | [] -> [], j_val hj
 	      | arg :: args -> 
-		if e_conv env.ExtraEnv.env evdref (j_val hj) arg then
-		  args, nf_evar !evdref (j_val hj)
-		else [], j_val hj
+                begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with
+                  | Some sigma -> evdref := sigma;
+                    args, nf_evar !evdref (j_val hj)
+                  | None ->
+                    [], j_val hj
+                end
 	    in
             let ujval = adjust_evar_source evdref na ujval in
 	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
@@ -1166,10 +1173,12 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
 	match valcon with
 	| None -> tj
 	| Some v ->
-	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
-	    else
+          begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with
+            | Some sigma -> evdref := sigma; tj
+            | None ->
 	      error_unexpected_type
                 ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+          end
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let env = make_env env sigma in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index aaec73f04..da72d7a75 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -69,10 +69,12 @@ let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv =
          | _ ->
              error_cant_apply_not_functional env !evdref funj argjv
        in
-       if Evarconv.e_cumul env evdref hj.uj_type c1 then
-         apply_rec (n+1) (subst1 hj.uj_val c2) restjl
-       else
-         error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       begin match Evarconv.cumul env !evdref hj.uj_type c1 with
+         | Some sigma -> evdref := sigma;
+           apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+         | None ->
+           error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       end
   in
   apply_rec 1 funj.uj_type (Array.to_list argjv)
 
@@ -93,20 +95,24 @@ let e_judge_of_apply env evdref funj argjv =
          | _ ->
             error_cant_apply_not_functional env !evdref funj argjv
        in
-       if Evarconv.e_cumul env evdref hj.uj_type c1 then
-         apply_rec (n+1) (subst1 hj.uj_val c2) restjl
-       else
-         error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       begin match Evarconv.cumul env !evdref hj.uj_type c1 with
+         | Some sigma -> evdref := sigma;
+           apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+         | None ->
+           error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       end
   in
   apply_rec 1 funj.uj_type (Array.to_list argjv)
 
-let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
+let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
-    error_number_branches env !evdref cj (Array.length explft);
-  for i = 0 to Array.length explft - 1 do
-    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
-      error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
-  done
+    error_number_branches env sigma cj (Array.length explft);
+  Array.fold_left2_i (fun i sigma lfj explft ->
+      match Evarconv.cumul env sigma lfj.uj_type explft with
+      | Some sigma -> sigma
+      | None ->
+        error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft)
+    sigma lfj explft
 
 let max_sort l =
   if Sorts.List.mem InType l then InType else
@@ -120,8 +126,11 @@ let e_is_correct_arity env evdref c pj ind specif params =
     let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref a1 a1') then error ();
-        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+      begin match Evarconv.cumul env !evdref a1 a1' with
+        | None -> error ()
+        | Some sigma -> evdref := sigma;
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+      end
     | Sort s, [] ->
         let s = ESorts.kind !evdref s in
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
@@ -167,19 +176,21 @@ let e_judge_of_case env evdref ci pj cj lfj =
   let indspec = ((ind, EInstance.kind !evdref u), spec) in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
-  e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
+  evdref := check_branch_types env !evdref (fst indspec) cj (lfj,bty);
   { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
-let check_type_fixpoint ?loc env evdref lna lar vdefj =
+let check_type_fixpoint ?loc env sigma lna lar vdefj =
   let lt = Array.length vdefj in
-    if Int.equal (Array.length lar) lt then
-      for i = 0 to lt-1 do
-        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body ?loc env !evdref
-            i lna vdefj lar
-      done
+  assert (Int.equal (Array.length lar) lt);
+  Array.fold_left2_i (fun i sigma defj ar ->
+      match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with
+      | Some sigma -> sigma
+      | None ->
+        error_ill_typed_rec_body ?loc env sigma
+          i lna vdefj lar)
+    sigma vdefj lar
+
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
@@ -194,10 +205,12 @@ let check_allowed_sort env sigma ind c p =
 
 let e_judge_of_cast env evdref cj k tj =
   let expected_type = tj.utj_val in
-  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+  match Evarconv.cumul env !evdref cj.uj_type expected_type with
+  | None ->
     error_actual_type_core env !evdref cj expected_type;
-  { uj_val = mkCast (cj.uj_val, k, expected_type);
-    uj_type = expected_type }
+  | Some sigma -> evdref := sigma;
+    { uj_val = mkCast (cj.uj_val, k, expected_type);
+      uj_type = expected_type }
 
 let enrich_env env evdref =
   let penv = Environ.pre_env env in
@@ -374,7 +387,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
   let vdefv = Array.map j_val vdefj in
-  let _ = check_type_fixpoint env1 evdref names lara vdefj in
+  evdref := check_type_fixpoint env1 !evdref names lara vdefj;
   (names,lara,vdefv)
 
 and execute_array env evdref = Array.map (execute env evdref)
@@ -382,8 +395,10 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+  match Evarconv.cumul env !evdref j.uj_type t with
+  | None ->
     error_actual_type_core env !evdref j t
+  | Some sigma -> evdref := sigma
 
 (* Type of a constr *)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 4905adf1f..2239dda5f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -46,8 +46,8 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
 
 (** Raise an error message if bodies have types not unifiable with the
     expected ones *)
-val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref ->
-  Names.Name.t array -> types array -> unsafe_judgment array -> unit
+val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ->
+  Names.Name.t array -> types array -> unsafe_judgment array -> evar_map
 
 val judge_of_prop : unsafe_judgment
 val judge_of_set : unsafe_judgment
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 66505edb5..60070e6fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3813,7 +3813,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
@@ -4366,7 +4369,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 *)
-- 
cgit v1.2.3


From 8894e9eb35e5529966fea699014fef83e4b270bd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:29:34 +0200
Subject: set_solve_evars doesn't use an evar_map ref

---
 pretyping/evarconv.ml  | 13 +++++++------
 pretyping/evarconv.mli |  2 +-
 pretyping/typing.ml    |  7 ++++++-
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2144639d5..49c429458 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1159,17 +1159,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
 
   let subst = make_subst (ctxt,Array.to_list args,argoccs) in
 
-  let evdref = ref evd in
-  let rhs = set_holes evdref rhs subst in
-  let evd = !evdref in
+  let evd, rhs =
+    let evdref = ref evd in
+    let rhs = set_holes evdref rhs subst in
+    !evdref, rhs
+  in
 
   (* We instantiate the evars of which the value is forced by typing *)
   let evd,rhs =
-    let evdref = ref evd in
-    try let c = !solve_evars env_evar evdref rhs in !evdref,c
+    try !solve_evars env_evar evd rhs
     with e when Pretype_errors.precatchable_exception e ->
       (* Could not revert all subterms *)
-      raise (TypingFailed !evdref) in
+      raise (TypingFailed evd) in
 
   let rec abstract_free_holes evd = function
   | (id,idty,c,_,evsref,_,_)::l ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index bea3eeb2e..cdf5dd0e5 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -69,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map ->
 
 (** Declare function to enforce evars resolution by using typing constraints *)
 
-val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
+val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
 
 type unify_fun = transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index da72d7a75..281e33e9b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -443,4 +443,9 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
+let solve_evars env sigma c =
+  let evdref = ref sigma in
+  let c = e_solve_evars env evdref c in
+  !evdref, c
+
+let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c)
-- 
cgit v1.2.3


From 5b432bf03f623b144871181446c68479482abe32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:44:30 +0200
Subject: Deprecate Refiner [evar_map ref] exported functions.

Uses internal to Refiner remain.
---
 plugins/ssr/ssrfwd.ml       | 4 +---
 plugins/ssr/ssrtacticals.ml | 5 ++---
 proofs/refiner.mli          | 3 +++
 proofs/tacmach.ml           | 2 ++
 proofs/tacmach.mli          | 3 +++
 tactics/eauto.ml            | 7 +++----
 6 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 6e17e8e15..c6beb08c5 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -184,9 +184,7 @@ let havetac ist
      let gs =
        List.map (fun (_,a) ->
          Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in
-     let tacopen_skols gl =
-        let stuff, g = Refiner.unpackage gl in
-        Refiner.repackage stuff (gs @ [g]) in
+     let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in
      let gl, ty = pf_e_type_of gl t in
      gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id,
        Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac)
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 9cc4f5cec..937e68b06 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -32,9 +32,8 @@ let get_index = function ArgArg i -> i | _ ->
 
 let tclPERM perm tac gls =
   let subgls = tac gls in
-  let sigma, subgll = Refiner.unpackage subgls in
-  let subgll' = perm subgll in
-  Refiner.repackage sigma subgll'
+  let subgll' = perm subgls.Evd.it in
+  re_sig subgll' subgls.Evd.sigma
 
 let rot_hyps dir i hyps =
   let n = List.length hyps in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5cd703a25..0f83e16ec 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -23,9 +23,12 @@ val pf_env  : goal sigma -> Environ.env
 val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 
 val refiner : rule -> tactic
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1889054f8..c1d69dfc5 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -33,9 +33,11 @@ let re_sig it  gc = { it = it; sigma = gc; }
 type 'a sigma   = 'a Evd.sigma;;
 type tactic     = Proof_type.tactic;;
 
+[@@@ocaml.warning "-3"]
 let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
+[@@@ocaml.warning "+3"]
 
 let sig_it   = Refiner.sig_it
 let project  = Refiner.project
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de96f8510..31496fb3d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,9 +30,12 @@ val project : goal sigma -> evar_map
 val re_sig : 'a -> evar_map -> 'a sigma
 
 val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c542..2408b8f2b 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 =
-- 
cgit v1.2.3


From e68f8c904b7ee8fee9f98f75e37ab6d01b54731f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:49:08 +0200
Subject: Typing: define functional alternatives to e_* functions

---
 pretyping/typing.ml  | 10 ++++++++++
 pretyping/typing.mli |  3 +++
 2 files changed, 13 insertions(+)

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 281e33e9b..5477d804a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -400,6 +400,11 @@ let e_check env evdref c t =
     error_actual_type_core env !evdref j t
   | Some sigma -> evdref := sigma
 
+let check env sigma c t =
+  let evdref = ref sigma in
+  e_check env evdref c t;
+  !evdref
+
 (* Type of a constr *)
 
 let unsafe_type_of env evd c =
@@ -416,6 +421,11 @@ let e_sort_of env evdref c =
   let a = e_type_judgment env evdref j in
   a.utj_type
 
+let sort_of env sigma c =
+  let evdref = ref sigma in
+  let a = e_sort_of env evdref c in
+  !evdref, a
+
 (* Try to solve the existential variables by typing *)
 
 let type_of ?(refresh=false) env evd c =
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 2239dda5f..da05102f2 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -28,15 +28,18 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
+val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
 val e_sort_of : env -> evar_map ref -> types -> Sorts.t
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
+val check : env -> evar_map -> constr -> types -> evar_map
 val e_check   : env -> evar_map ref -> constr -> types -> unit
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
+val solve_evars : env -> evar_map -> constr -> evar_map * constr
 val e_solve_evars : env -> evar_map ref -> constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
-- 
cgit v1.2.3


From c22ac10752c12bcb23402ad29a73f2d9699248a6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 15:03:10 +0200
Subject: Deprecate Typing.e_* functions

---
 plugins/cc/cctac.ml                            |  7 +++----
 plugins/funind/functional_principles_proofs.ml |  3 ++-
 plugins/funind/functional_principles_types.ml  |  6 ++++--
 plugins/funind/indfun.ml                       |  3 ++-
 plugins/funind/invfun.ml                       |  6 ++++--
 plugins/ltac/evar_tactics.ml                   |  4 +---
 plugins/ltac/rewrite.ml                        |  7 +++----
 plugins/ltac/tacinterp.ml                      |  6 ++----
 plugins/setoid_ring/newring.ml                 | 17 +++++++++++------
 pretyping/coercion.ml                          |  8 +++++---
 pretyping/typing.mli                           |  4 ++++
 proofs/refine.ml                               | 23 ++++++++---------------
 tactics/tactics.ml                             | 16 +++++++---------
 vernac/comFixpoint.ml                          |  4 +---
 vernac/comProgramFixpoint.ml                   |  4 +---
 15 files changed, 58 insertions(+), 60 deletions(-)

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c4db49cd3..361981c5b 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -49,7 +49,7 @@ let whd_delta env sigma t =
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) c
+let sf_of env sigma c = snd (sort_of env sigma c)
 
 let rec decompose_term env sigma t=
     match EConstr.kind sigma (whd env sigma t) with
@@ -264,9 +264,8 @@ let app_global_with_holes f args n =
       let ans = mkApp (fc, args) in
       let (sigma, holes) = gen_holes env sigma t n [] in
       let ans = applist (ans, holes) in
-      let evdref = ref sigma in
-      let () = Typing.e_check env evdref ans concl in
-      (!evdref, ans)
+      let sigma = Typing.check env sigma ans concl in
+      (sigma, ans)
     end
   end
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a0616b308..44fa0740d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1051,7 +1051,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
       evd:=evd';
-      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
+      let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in
+      evd := sigma;
       res
   in
   let nb_intro_to_do = nb_prod (project g) (pf_concl g) in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 04a23cdb9..dc0f240bd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -291,7 +291,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
   in
-  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
+  let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
+  evd := sigma;
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
@@ -630,7 +631,8 @@ let build_scheme fas =
 	    in
             let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
-            let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in
+            let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in
+            evd := sigma;
             let c, u =
               try EConstr.destConst !evd f
               with DestKO ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 7df57b577..efbd029e4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -385,7 +385,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
-             let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
+             let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in
+             evd := sigma;
 	     let princ_type = EConstr.Unsafe.to_constr princ_type in
     	     Functional_principles_types.generate_functional_principle
 	       evd
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 28e85268a..094f54156 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -103,7 +103,8 @@ let generate_type evd g_to_f f graph i =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd !evd graph)))
   in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
+  evd := sigma;
   let ctxt,_ = decompose_prod_assum !evd graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -769,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+         let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
+         evd := sigma;
 	   let type_of_lemma = nf_zeta type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 9382f567b..fb6be430f 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -85,9 +85,7 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    let sigma = ref sigma in
-    let _ = Typing.e_sort_of env sigma typ in
-    let sigma = !sigma in
+    let sigma, _ = Typing.sort_of env sigma typ in
     let id = match name with
     | Name.Anonymous ->
       let id = Namegen.id_of_name_using_hdchar env sigma typ name in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9eb55aa5e..1b86583da 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -104,9 +104,8 @@ let extends_undefined evars evars' =
 
 let app_poly_check env evars f args =
   let (evars, cstrs), fc = f evars in
-  let evdref = ref evars in 
-  let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
-    (!evdref, cstrs), t
+  let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in
+  (evars, cstrs), t
 
 let app_poly_nocheck env evars f args =
   let evars, fc = f evars in 
@@ -1469,8 +1468,8 @@ exception RewriteFailure of Pp.t
 type result = (evar_map * constr option * types) option option
 
 let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
+  let sigma, sort = Typing.sort_of env sigma concl in
   let evdref = ref sigma in
-  let sort = Typing.e_sort_of env evdref concl in
   let evars = (!evdref, Evar.Set.empty) in
   let evars, cstr =
     let prop, (evars, arrow) = 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 84049d4ed..a93cf5ae7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -691,11 +691,9 @@ let interp_may_eval f ist env sigma = function
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let ctxt = EConstr.Unsafe.to_constr ctxt in
-	let evdref = ref sigma in
-	let ic = EConstr.Unsafe.to_constr ic in
+        let ic = EConstr.Unsafe.to_constr ic in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
-	!evdref , c
+        Typing.solve_evars env sigma (EConstr.of_constr c)
       with
 	| Not_found ->
 	    user_err ?loc ~hdr:"interp_may_eval"
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b2ac3b5a4..074fcb92e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -505,10 +505,12 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	let op_morph =
 	  match opp with
               Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
-            | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
-	let setoid = Typing.e_solve_evars env evd setoid in
-	let op_morph = Typing.e_solve_evars env evd op_morph in
-	  (setoid,op_morph)
+          | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+        let sigma = !evd in
+        let sigma, setoid = Typing.solve_evars env sigma setoid in
+        let sigma, op_morph = Typing.solve_evars env sigma op_morph in
+        evd := sigma;
+        (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
@@ -595,7 +597,8 @@ let make_hyp_list env evdref lH =
       (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
       (plapp evdref coq_nil [|carrier|])
   in 
-  let l' = Typing.e_solve_evars env evdref l in
+  let sigma, l' = Typing.solve_evars env !evdref l in
+  evdref := sigma;
   let l' = EConstr.Unsafe.to_constr l' in
     Evarutil.nf_evars_universes !evdref l'
 
@@ -733,7 +736,9 @@ let make_term_list env evd carrier rl =
   let l = List.fold_right
     (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
     (plapp evd coq_nil [|carrier|])
-  in Typing.e_solve_evars env evd l
+  in
+  let sigma, l = Typing.solve_evars env !evd l in
+  evd := sigma; l
 
 let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ea8557b18..c9c2445a7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -197,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some (fun x -> 
 	  let term = co x in
-	    Typing.e_solve_evars env evdref term)
+          let sigma, term = Typing.solve_evars env !evdref term in
+          evdref := sigma; term)
       in
 	if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
 	  (* Second-order unification needed. *)
@@ -343,8 +344,9 @@ let app_coercion env evdref coercion v =
   match coercion with
   | None -> v
   | Some f ->
-     let v' = Typing.e_solve_evars env evdref (f v) in
-     whd_betaiota !evdref v'
+    let sigma, v' = Typing.solve_evars env !evdref (f v) in
+    evdref := sigma;
+    whd_betaiota !evdref v'
 
 let coerce_itf ?loc env evd v t c1 =
   let evdref = ref evd in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index da05102f2..3cf43ace0 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -26,14 +26,17 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 
 (** Variant of [type_of] using references instead of state-passing. *)
 val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
+[@@ocaml.deprecated "Use [Typing.type_of]"]
 
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
 val e_sort_of : env -> evar_map ref -> types -> Sorts.t
+[@@ocaml.deprecated "Use [Typing.sort_of]"]
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
 val check : env -> evar_map -> constr -> types -> evar_map
 val e_check   : env -> evar_map ref -> constr -> types -> unit
+[@@ocaml.deprecated "Use [Typing.check]"]
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
@@ -41,6 +44,7 @@ val meta_type : evar_map -> metavariable -> types
 (** Solve existential variables using typing *)
 val solve_evars : env -> evar_map -> constr -> evar_map * constr
 val e_solve_evars : env -> evar_map ref -> constr -> constr
+[@@ocaml.deprecated "Use [Typing.solve_evars]"]
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 5a2d82977..b64e7a2e5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -30,26 +30,19 @@ let typecheck_evar ev env sigma =
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
     let t = NamedDecl.get_type decl in
-    let evdref = ref sigma in
-    let _ = Typing.e_sort_of env evdref t in
-    let () = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    let sigma, _ = Typing.sort_of env sigma t in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,body,_) -> Typing.check env sigma body t
     in
-    (!evdref, EConstr.push_named decl env)
+    (sigma, EConstr.push_named decl env)
   in
   let (common, changed) = extract_prefix env info in
   let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
-  let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
-  !evdref
-
-let typecheck_proof c concl env sigma =
-  let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
-  !evdref
+  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
+  sigma
 
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
@@ -93,7 +86,7 @@ let generic_refine ~typecheck f gl =
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
+  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 60070e6fe..01351e249 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1985,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))
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 7b382dacc..85c0699ea 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -199,9 +199,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
              try
                let sigma, h_term = fix_proto sigma in
                let app = mkApp (h_term, [|sort; t|]) in
-               let _evd = ref sigma in
-               let res = Typing.e_solve_evars env _evd app in
-               !_evd, res
+               Typing.solve_evars env sigma app
              with e when CErrors.noncritical e -> sigma, t
            in
            sigma, LocalAssum (id,fixprot) :: env'
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 745f1df1d..349fc562b 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -190,9 +190,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
     sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
   in
-  let _evd = ref sigma in
-  let def = Typing.e_solve_evars env _evd def in
-  let sigma = !_evd in
+  let sigma, def = Typing.solve_evars env sigma def in
   let sigma = Evarutil.nf_evar_map sigma in
   let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context sigma binders_rel in
-- 
cgit v1.2.3


From 0bae2ad1082e6bf7ef24ae4767d6f7cfd8c1a973 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 15:31:46 +0200
Subject: Typing implementation doesn't use evdref.

---
 pretyping/typing.ml | 371 +++++++++++++++++++++++++---------------------------
 1 file changed, 179 insertions(+), 192 deletions(-)

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5477d804a..6bd75c93d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -37,72 +37,72 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
   Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
 
-let e_type_judgment env evdref j =
-  match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
-    | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s }
+let type_judgment env sigma j =
+  match EConstr.kind sigma (whd_all env sigma j.uj_type) with
+    | Sort s -> sigma, {utj_val = j.uj_val; utj_type = ESorts.kind sigma s }
     | Evar ev ->
-        let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
-        evdref := evd; { utj_val = j.uj_val; utj_type = s }
-    | _ -> error_not_a_type env !evdref j
-
-let e_assumption_of_judgment env evdref j =
-  try (e_type_judgment env evdref j).utj_val
+        let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in
+        sigma, { utj_val = j.uj_val; utj_type = s }
+    | _ -> error_not_a_type env sigma j
+
+let assumption_of_judgment env sigma j =
+  try
+    let sigma, j = type_judgment env sigma j in
+    sigma, j.utj_val
   with Type_errors.TypeError _ | PretypeError _ ->
-    error_assumption env !evdref j
+    error_assumption env sigma j
 
-let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv =
-  let rec apply_rec n typ = function
+let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
+  let rec apply_rec sigma n typ = function
   | [] ->
-      { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
-        uj_type =
-          let ar = inductive_type_knowing_parameters env !evdref ind argjv in
-          hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) }
+      sigma, { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
+               uj_type =
+                 let ar = inductive_type_knowing_parameters env sigma ind argjv in
+                 hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) }
   | hj::restjl ->
-       let (c1,c2) =
-         match EConstr.kind !evdref (whd_all env !evdref typ) with
-         | Prod (_,c1,c2) -> (c1,c2)
+       let sigma, (c1,c2) =
+         match EConstr.kind sigma (whd_all env sigma typ) with
+         | Prod (_,c1,c2) -> sigma, (c1,c2)
          | Evar ev ->
-             let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
-             evdref := evd';
-             let (_,c1,c2) = destProd evd' t in
-             (c1,c2)
+             let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
+             let (_,c1,c2) = destProd sigma t in
+             sigma, (c1,c2)
          | _ ->
-             error_cant_apply_not_functional env !evdref funj argjv
+             error_cant_apply_not_functional env sigma funj argjv
        in
-       begin match Evarconv.cumul env !evdref hj.uj_type c1 with
-         | Some sigma -> evdref := sigma;
-           apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+       begin match Evarconv.cumul env sigma hj.uj_type c1 with
+         | Some sigma ->
+           apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
          | None ->
-           error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+           error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
        end
   in
-  apply_rec 1 funj.uj_type (Array.to_list argjv)
+  apply_rec sigma 1 funj.uj_type (Array.to_list argjv)
 
-let e_judge_of_apply env evdref funj argjv =
-  let rec apply_rec n typ = function
+let judge_of_apply env sigma funj argjv =
+  let rec apply_rec sigma n typ = function
   | [] ->
-      { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
-        uj_type = typ }
+    sigma, { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
+             uj_type = typ }
   | hj::restjl ->
-       let (c1,c2) =
-         match EConstr.kind !evdref (whd_all env !evdref typ) with
-         | Prod (_,c1,c2) -> (c1,c2)
+       let sigma, (c1,c2) =
+         match EConstr.kind sigma (whd_all env sigma typ) with
+         | Prod (_,c1,c2) -> sigma, (c1,c2)
          | Evar ev ->
-             let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
-             evdref := evd';
-             let (_,c1,c2) = destProd evd' t in
-             (c1,c2)
+             let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
+             let (_,c1,c2) = destProd sigma t in
+             sigma, (c1,c2)
          | _ ->
-            error_cant_apply_not_functional env !evdref funj argjv
+            error_cant_apply_not_functional env sigma funj argjv
        in
-       begin match Evarconv.cumul env !evdref hj.uj_type c1 with
-         | Some sigma -> evdref := sigma;
-           apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+       begin match Evarconv.cumul env sigma hj.uj_type c1 with
+         | Some sigma ->
+           apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
          | None ->
-           error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+           error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
        end
   in
-  apply_rec 1 funj.uj_type (Array.to_list argjv)
+  apply_rec sigma 1 funj.uj_type (Array.to_list argjv)
 
 let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
@@ -118,32 +118,34 @@ let max_sort l =
   if Sorts.List.mem InType l then InType else
   if Sorts.List.mem InSet l then InSet else InProp
 
-let e_is_correct_arity env evdref c pj ind specif params =
-  let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in
+let is_correct_arity env sigma c pj ind specif params =
+  let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
-  let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
-  let rec srec env pt ar =
-    let pt' = whd_all env !evdref pt in
-    match EConstr.kind !evdref pt', ar with
+  let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in
+  let rec srec env sigma pt ar =
+    let pt' = whd_all env sigma pt in
+    match EConstr.kind sigma pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-      begin match Evarconv.cumul env !evdref a1 a1' with
+      begin match Evarconv.cumul env sigma a1 a1' with
         | None -> error ()
-        | Some sigma -> evdref := sigma;
-          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+        | Some sigma ->
+          srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar'
       end
     | Sort s, [] ->
-        let s = ESorts.kind !evdref s in
+        let s = ESorts.kind sigma s in
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
+        else sigma
     | Evar (ev,_), [] ->
-        let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
-        evdref := Evd.define ev (mkSort s) evd
+        let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in
+        let sigma = Evd.define ev (mkSort s) sigma in
+        sigma
     | _, (LocalDef _ as d)::ar' ->
-        srec (push_rel d env) (lift 1 pt') ar'
+        srec (push_rel d env) sigma (lift 1 pt') ar'
     | _ ->
         error ()
   in
-  srec env pj.uj_type (List.rev arsign)
+  srec env sigma pj.uj_type (List.rev arsign)
 
 let lambda_applist_assum sigma n c l =
   let rec app n subst t l =
@@ -156,29 +158,29 @@ let lambda_applist_assum sigma n c l =
     | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
   app n [] c l
 
-let e_type_case_branches env evdref (ind,largs) pj c =
+let type_case_branches env sigma (ind,largs) pj c =
   let specif = lookup_mind_specif env (fst ind) in
   let nparams = inductive_params specif in
   let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
   let params = List.map EConstr.Unsafe.to_constr params in
-  let () = e_is_correct_arity env evdref c pj ind specif params in
-  let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in
+  let sigma = is_correct_arity env sigma c pj ind specif params in
+  let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
   let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
-  let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
-  (lc, ty)
+  let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
+  sigma, (lc, ty)
 
-let e_judge_of_case env evdref ci pj cj lfj =
+let judge_of_case env sigma ci pj cj lfj =
   let ((ind, u), spec) =
-    try find_mrectype env !evdref cj.uj_type
-    with Not_found -> error_case_not_inductive env !evdref cj in
-  let indspec = ((ind, EInstance.kind !evdref u), spec) in
+    try find_mrectype env sigma cj.uj_type
+    with Not_found -> error_case_not_inductive env sigma cj in
+  let indspec = ((ind, EInstance.kind sigma u), spec) in
   let _ = check_case_info env (fst indspec) ci in
-  let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
-  evdref := check_branch_types env !evdref (fst indspec) cj (lfj,bty);
-  { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
-    uj_type = rslty }
+  let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in
+  let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in
+  sigma, { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
+           uj_type = rslty }
 
 let check_type_fixpoint ?loc env sigma lna lar vdefj =
   let lt = Array.length vdefj in
@@ -203,19 +205,19 @@ let check_allowed_sort env sigma ind c p =
     error_elim_arity env sigma ind sorts c pj
       (Some(ksort,s,Type_errors.error_elim_explain ksort s))
 
-let e_judge_of_cast env evdref cj k tj =
+let judge_of_cast env sigma cj k tj =
   let expected_type = tj.utj_val in
-  match Evarconv.cumul env !evdref cj.uj_type expected_type with
+  match Evarconv.cumul env sigma cj.uj_type expected_type with
   | None ->
-    error_actual_type_core env !evdref cj expected_type;
-  | Some sigma -> evdref := sigma;
-    { uj_val = mkCast (cj.uj_val, k, expected_type);
-      uj_type = expected_type }
+    error_actual_type_core env sigma cj expected_type;
+  | Some sigma ->
+    sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
+             uj_type = expected_type }
 
-let enrich_env env evdref =
+let enrich_env env sigma =
   let penv = Environ.pre_env env in
   let penv' = Pre_env.({ penv with env_stratification =
-    { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
+    { penv.env_stratification with env_universes = Evd.universes sigma } }) in
   Environ.env_of_pre_env penv'
 
 let check_fix env sigma pfix =
@@ -280,182 +282,167 @@ let judge_of_letin env name defj typj j =
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
-let rec execute env evdref cstr =
-  let cstr = whd_evar !evdref cstr in
-  match EConstr.kind !evdref cstr with
+let rec execute env sigma cstr =
+  let cstr = whd_evar sigma cstr in
+  match EConstr.kind sigma cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = meta_type !evdref n }
+        sigma, { uj_val = cstr; uj_type = meta_type sigma n }
 
     | Evar ev ->
-	let ty = EConstr.existential_type !evdref ev in
-	let jty = execute env evdref ty in
-	let jty = e_assumption_of_judgment env evdref jty in
-	{ uj_val = cstr; uj_type = jty }
+        let ty = EConstr.existential_type sigma ev in
+        let sigma, jty = execute env sigma ty in
+        let sigma, jty = assumption_of_judgment env sigma jty in
+        sigma, { uj_val = cstr; uj_type = jty }
 
     | Rel n ->
-	judge_of_relative env n
+        sigma, judge_of_relative env n
 
     | Var id ->
-        judge_of_variable env id
+        sigma, judge_of_variable env id
 
     | Const (c, u) ->
-        let u = EInstance.kind !evdref u in
-        make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
+        let u = EInstance.kind sigma u in
+        sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
 
     | Ind (ind, u) ->
-        let u = EInstance.kind !evdref u in
-	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
+        let u = EInstance.kind sigma u in
+        sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
 
     | Construct (cstruct, u) ->
-        let u = EInstance.kind !evdref u in
-	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
+        let u = EInstance.kind sigma u in
+        sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
 
     | Case (ci,p,c,lf) ->
-        let cj = execute env evdref c in
-        let pj = execute env evdref p in
-        let lfj = execute_array env evdref lf in
-        e_judge_of_case env evdref ci pj cj lfj
+        let sigma, cj = execute env sigma c in
+        let sigma, pj = execute env sigma p in
+        let sigma, lfj = execute_array env sigma lf in
+        judge_of_case env sigma ci pj cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
-        let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
+        let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
 	let fix = (vni,recdef') in
-        check_fix env !evdref fix;
-	make_judge (mkFix fix) tys.(i)
+        check_fix env sigma fix;
+        sigma, make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
-        let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
+        let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
         let cofix = (i,recdef') in
-        check_cofix env !evdref cofix;
-	make_judge (mkCoFix cofix) tys.(i)
+        check_cofix env sigma cofix;
+        sigma, make_judge (mkCoFix cofix) tys.(i)
 
     | Sort s ->
-      begin match ESorts.kind !evdref s with
+      begin match ESorts.kind sigma s with
       | Prop c ->
-        judge_of_prop_contents c
+        sigma, judge_of_prop_contents c
       | Type u ->
-        judge_of_type u
+        sigma, judge_of_type u
       end
 
     | Proj (p, c) -> 
-        let cj = execute env evdref c in
-	  judge_of_projection env !evdref p cj
+      let sigma, cj = execute env sigma c in
+      sigma, judge_of_projection env sigma p cj
 
     | App (f,args) ->
-        let jl = execute_array env evdref args in
-        (match EConstr.kind !evdref f with
+        let sigma, jl = execute_array env sigma args in
+        (match EConstr.kind sigma f with
             | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
-               let fj = execute env evdref f in
-               e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl
+               let sigma, fj = execute env sigma f in
+               judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl
             | _ ->
                (* No template polymorphism *)
-               let fj = execute env evdref f in
-               e_judge_of_apply env evdref fj jl)
+               let sigma, fj = execute env sigma f in
+               judge_of_apply env sigma fj jl)
 
     | Lambda (name,c1,c2) ->
-        let j = execute env evdref c1 in
-	let var = e_type_judgment env evdref j in
+        let sigma, j = execute env sigma c1 in
+        let sigma, var = type_judgment env sigma j in
 	let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
-        let j' = execute env1 evdref c2 in
-        judge_of_abstraction env1 name var j'
+        let sigma, j' = execute env1 sigma c2 in
+        sigma, judge_of_abstraction env1 name var j'
 
     | Prod (name,c1,c2) ->
-        let j = execute env evdref c1 in
-        let varj = e_type_judgment env evdref j in
+        let sigma, j = execute env sigma c1 in
+        let sigma, varj = type_judgment env sigma j in
 	let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
-        let j' = execute env1 evdref c2 in
-        let varj' = e_type_judgment env1 evdref j' in
-	judge_of_product env name varj varj'
+        let sigma, j' = execute env1 sigma c2 in
+        let sigma, varj' = type_judgment env1 sigma j' in
+        sigma, judge_of_product env name varj varj'
 
      | LetIn (name,c1,c2,c3) ->
-        let j1 = execute env evdref c1 in
-        let j2 = execute env evdref c2 in
-        let j2 = e_type_judgment env evdref j2 in
-        let _ =  e_judge_of_cast env evdref j1 DEFAULTcast j2 in
+        let sigma, j1 = execute env sigma c1 in
+        let sigma, j2 = execute env sigma c2 in
+        let sigma, j2 = type_judgment env sigma j2 in
+        let sigma, _ =  judge_of_cast env sigma j1 DEFAULTcast j2 in
         let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
-        let j3 = execute env1 evdref c3 in
-        judge_of_letin env name j1 j2 j3
+        let sigma, j3 = execute env1 sigma c3 in
+        sigma, judge_of_letin env name j1 j2 j3
 
     | Cast (c,k,t) ->
-        let cj = execute env evdref c in
-        let tj = execute env evdref t in
-	let tj = e_type_judgment env evdref tj in
-        e_judge_of_cast env evdref cj k tj
-
-and execute_recdef env evdref (names,lar,vdef) =
-  let larj = execute_array env evdref lar in
-  let lara = Array.map (e_assumption_of_judgment env evdref) larj in
+        let sigma, cj = execute env sigma c in
+        let sigma, tj = execute env sigma t in
+        let sigma, tj = type_judgment env sigma tj in
+        judge_of_cast env sigma cj k tj
+
+and execute_recdef env sigma (names,lar,vdef) =
+  let sigma, larj = execute_array env sigma lar in
+  let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdefj = execute_array env1 evdref vdef in
+  let sigma, vdefj = execute_array env1 sigma vdef in
   let vdefv = Array.map j_val vdefj in
-  evdref := check_type_fixpoint env1 !evdref names lara vdefj;
-  (names,lara,vdefv)
+  let sigma = check_type_fixpoint env1 sigma names lara vdefj in
+  sigma, (names,lara,vdefv)
 
-and execute_array env evdref = Array.map (execute env evdref)
+and execute_array env = Array.fold_left_map (execute env)
 
-let e_check env evdref c t =
-  let env = enrich_env env evdref in
-  let j = execute env evdref c in
-  match Evarconv.cumul env !evdref j.uj_type t with
+let check env sigma c t =
+  let env = enrich_env env sigma in
+  let sigma, j = execute env sigma c in
+  match Evarconv.cumul env sigma j.uj_type t with
   | None ->
-    error_actual_type_core env !evdref j t
-  | Some sigma -> evdref := sigma
+    error_actual_type_core env sigma j t
+  | Some sigma -> sigma
 
-let check env sigma c t =
-  let evdref = ref sigma in
-  e_check env evdref c t;
-  !evdref
+let e_check env evdref c t =
+  evdref := check env !evdref c t
 
 (* Type of a constr *)
 
-let unsafe_type_of env evd c =
-  let evdref = ref evd in
-  let env = enrich_env env evdref in
-  let j = execute env evdref c in
-    j.uj_type
+let unsafe_type_of env sigma c =
+  let env = enrich_env env sigma in
+  let sigma, j = execute env sigma c in
+  j.uj_type
 
 (* Sort of a type *)
 
-let e_sort_of env evdref c =
-  let env = enrich_env env evdref in
-  let j = execute env evdref c in
-  let a = e_type_judgment env evdref j in
-  a.utj_type
-
 let sort_of env sigma c =
-  let evdref = ref sigma in
-  let a = e_sort_of env evdref c in
-  !evdref, a
+  let env = enrich_env env sigma in
+  let sigma, j = execute env sigma c in
+  let sigma, a = type_judgment env sigma j in
+  sigma, a.utj_type
+
+let e_sort_of env evdref c =
+  Evarutil.evd_comb1 (sort_of env) evdref c
 
 (* Try to solve the existential variables by typing *)
 
-let type_of ?(refresh=false) env evd c =
-  let evdref = ref evd in
-  let env = enrich_env env evdref in
-  let j = execute env evdref c in
+let type_of ?(refresh=false) env sigma c =
+  let env = enrich_env env sigma in
+  let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
-    else !evdref, j.uj_type
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type
+    else sigma, j.uj_type
 
-let e_type_of ?(refresh=false) env evdref c =
-  let env = enrich_env env evdref in
-  let j = execute env evdref c in
-  (* side-effect on evdref *)
-    if refresh then
-      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
-      let () = evdref := evd in
-      c
-    else j.uj_type
+let e_type_of ?refresh env evdref c =
+  Evarutil.evd_comb1 (type_of ?refresh env) evdref c
 
-let e_solve_evars env evdref c =
-  let env = enrich_env env evdref in
-  let c = (execute env evdref c).uj_val in
+let solve_evars env sigma c =
+  let env = enrich_env env sigma in
+  let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
-  nf_evar !evdref c
+  sigma, nf_evar sigma j.uj_val
 
-let solve_evars env sigma c =
-  let evdref = ref sigma in
-  let c = e_solve_evars env evdref c in
-  !evdref, c
+let e_solve_evars env evdref c =
+  Evarutil.evd_comb1 (solve_evars env) evdref c
 
 let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c)
-- 
cgit v1.2.3


From 9f175bbeb19175a1e422225986f139e8f1a1b56c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 4 May 2018 14:36:18 +0200
Subject: Use evd_combX in Cases.

---
 engine/evarutil.ml  | 10 +++++-----
 engine/evarutil.mli | 22 +++++++++++++---------
 pretyping/cases.ml  | 46 +++++++++++++++++++---------------------------
 3 files changed, 37 insertions(+), 41 deletions(-)

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 52610f6f3..2b202ef3e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -436,7 +436,7 @@ let new_pure_evar_full evd evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -463,14 +463,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
   in
   (evd, newevk)
 
-let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
+let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
@@ -480,7 +480,7 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ =
+let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ =
   let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -490,7 +490,7 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnami
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid =
+let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
   let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
   evd', (e, s)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c24660f5b..7dd98bac9 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -25,10 +25,11 @@ val mk_new_meta : unit -> constr
 (** {6 Creating a fresh evar given their type and context} *)
 
 val new_evar_from_context :
-  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * EConstr.t
+  ?principal:bool ->
+  named_context_val -> evar_map  -> types -> evar_map * EConstr.t
 
 type naming_mode =
   | KeepUserNameAndRenameExistingButSectionNames
@@ -37,25 +38,28 @@ type naming_mode =
   | FailIfConflict
 
 val new_evar :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t
+  ?principal:bool -> ?hypnaming:naming_mode ->
+  env -> evar_map -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
-  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * Evar.t
+  ?principal:bool ->
+  named_context_val -> evar_map -> types -> evar_map * Evar.t
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> ?hypnaming:naming_mode -> rigid ->
+  ?principal:bool -> ?hypnaming:naming_mode ->
+  env -> evar_map -> rigid ->
   evar_map * (constr * Sorts.t)
 
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
@@ -74,10 +78,10 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> 
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
+ named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 84f0aba8c..ee7c39982 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -295,9 +295,11 @@ let inductive_template evdref env tmloc ind =
         | LocalAssum (na,ty) ->
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
-            let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in
-            evdref := evd;
-	    (e::subst,e::evarl,n+1)
+            let e = evd_comb1
+                (Evarutil.new_evar env ~src:(hole_source n))
+                evdref ty'
+            in
+            (e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
             let b = EConstr.of_constr b in
 	    (substl subst b::subst,evarl,n+1))
@@ -375,8 +377,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref !lvar tomatch in
-  let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in
-  evdref := evd;
+  let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in
   let typ = nf_evar !evdref j.uj_type in
   lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
   let t =
@@ -399,15 +400,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
-  let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in
-  evdref := evd;
+  let (e, u) = evd_comb1 (new_type_evar env  ~src:src) evdref univ_flexible_alg in
   e
 
-let evd_comb2 f evdref x y =
-  let (evd',y) = f !evdref x y in
-  evdref := evd';
-  y
-
 let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
@@ -1019,8 +1014,8 @@ let adjust_impossible_cases pb pred tomatch submat =
     begin match Constr.kind pred with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
         if not (Evd.is_defined !(pb.evdref) evk) then begin
-	  let evd, default = use_unit_judge !(pb.evdref) in
-          pb.evdref := Evd.define evk default.uj_type evd
+          let default = evd_comb0 use_unit_judge pb.evdref in
+          pb.evdref := Evd.define evk default.uj_type !(pb.evdref)
         end;
         add_assert_false_case pb tomatch
     | _ ->
@@ -1686,8 +1681,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let evd, ev' = Evarutil.new_evar env !evdref ~src ty in
-        evdref := evd;
+        let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1718,8 +1712,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	  (named_context extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
-      let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in
-      evdref := evd;
+      let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1731,14 +1724,15 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
            we are in an impossible branch *)
 	let n = Context.Rel.length (rel_context env) in
 	let n' = Context.Rel.length (rel_context tycon_env) in
-        let evd, (impossible_case_type, u) =
-          new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
-        evdref := evd;
-	(lift (n'-n) impossible_case_type, mkSort u)
+        let impossible_case_type, u =
+          evd_comb1
+            (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase))
+            evdref univ_flexible_alg
+        in
+        (lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.type_of extenv !evdref t in
-        evdref := evd;
+        let tt = evd_comb1 (Typing.type_of extenv) evdref t in
         (t,tt) in
   match cumul env !evdref tt (mkSort s) with
   | None -> anomaly (Pp.str "Build_tycon: should be a type.");
@@ -1932,9 +1926,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
 let inh_conv_coerce_to_tycon ?loc env evdref j tycon =
   match tycon with
     | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in
-          evdref := evd';
-          j
+      evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p
     | None -> j
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
-- 
cgit v1.2.3