Merge PR #7359: Reduce usage of evar_map references

2 files changed, 53 insertions, 42 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6c27d5937..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)
@@ -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 3bbd2923c..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,41 +38,31 @@ 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
@@ -79,7 +70,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
@@ -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"]