Merge PR coq#7359: Reduce usage of evar_map references

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)
@@ -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. *)

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,49 +38,38 @@ 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
 
-(** 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 :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?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
+  ?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
-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
 
 (** 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
@@ -88,10 +78,10 @@ val e_new_global : evar_map ref -> GlobRef.t -> 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
@@ -187,8 +177,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. *)
@@ -237,11 +225,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
 
@@ -276,3 +264,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"]

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
 

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";
@@ -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

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 ->

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

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

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

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) = 

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"