Removing the need of evarmaps in constr internalization.

Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.

14 files changed, 47 insertions, 56 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0a2a459d38..e9ebcf39f9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1329,7 +1329,7 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalize sigma globalenv env allow_patvar lvar c =
+let internalize globalenv env allow_patvar lvar c =
   let rec intern env = function
     | CRef ref as x ->
 	let (c,imp,subscopes,l),_ =
@@ -1534,7 +1534,6 @@ let internalize sigma globalenv env allow_patvar lvar c =
           let ist = {
             Genintern.ltacvars = lvars;
             ltacrecvars = Id.Map.empty;
-            gsigma = sigma;
             genv = globalenv;
           } in
           let (_, glb) = Genintern.generic_intern ist gen in
@@ -1715,18 +1714,18 @@ type ltac_sign = Id.Set.t * Id.Set.t
 
 let empty_ltac_sign = (Id.Set.empty, Id.Set.empty)
 
-let intern_gen kind sigma env
+let intern_gen kind env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
                c =
   let tmp_scope = scope_of_type_kind kind in
-  internalize sigma env {ids = extract_ids env; unb = false;
+  internalize env {ids = extract_ids env; unb = false;
 		         tmp_scope = tmp_scope; scopes = [];
 			 impls = impls}
     allow_patvar (ltacvars, Id.Map.empty) c
 
-let intern_constr sigma env c = intern_gen WithoutTypeConstraint sigma env c
+let intern_constr env c = intern_gen WithoutTypeConstraint env c
 
-let intern_type sigma env c = intern_gen IsType sigma env c
+let intern_type env c = intern_gen IsType env c
 
 let intern_pattern globalenv patt =
   try
@@ -1744,7 +1743,7 @@ let intern_pattern globalenv patt =
 (* All evars resolved *)
 
 let interp_gen kind sigma env ?(impls=empty_internalization_env) c =
-  let c = intern_gen kind ~impls sigma env c in
+  let c = intern_gen kind ~impls env c in
   understand ~expected_type:kind sigma env c
 
 let interp_constr sigma env ?(impls=empty_internalization_env) c =
@@ -1759,13 +1758,13 @@ let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
 (* Not all evars expected to be resolved *)
 
 let interp_open_constr sigma env c =
-  understand_tcc sigma env (intern_constr sigma env c)
+  understand_tcc sigma env (intern_constr env c)
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
 let interp_constr_evars_gen_impls evdref
     env ?(impls=empty_internalization_env) expected_type c =
-  let c = intern_gen expected_type ~impls !evdref env c in
+  let c = intern_gen expected_type ~impls env c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
     understand_tcc_evars evdref env ~expected_type c, imps
 
@@ -1781,7 +1780,7 @@ let interp_type_evars_impls evdref env ?(impls=empty_internalization_env) c =
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
 let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) expected_type c =
-  let c = intern_gen expected_type ~impls !evdref env c in
+  let c = intern_gen expected_type ~impls env c in
   understand_tcc_evars evdref env ~expected_type c
 
 let interp_constr_evars evdref env ?(impls=empty_internalization_env) c =
@@ -1795,16 +1794,16 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
 
 (* Miscellaneous *)
 
-let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
+let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
   let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
-            ~allow_patvar:true ~ltacvars sigma env c in
+            ~allow_patvar:true ~ltacvars env c in
   pattern_of_glob_constr c
 
 let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = Id.Map.map (fun typ -> (ref None, typ)) vars in
-  let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false;
+  let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
@@ -1819,25 +1818,25 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
 (* Interpret binders and contexts  *)
 
 let interp_binder sigma env na t =
-  let t = intern_gen IsType sigma env t in
+  let t = intern_gen IsType env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
   understand ~expected_type:IsType sigma env t'
 
 let interp_binder_evars evdref env na t =
-  let t = intern_gen IsType !evdref env t in
+  let t = intern_gen IsType env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
   understand_tcc_evars evdref env ~expected_type:IsType t'
 
 open Environ
 
-let my_intern_constr sigma env lvar acc c =
-  internalize sigma env acc false lvar c
+let my_intern_constr env lvar acc c =
+  internalize env acc false lvar c
 
-let intern_context global_level sigma env impl_env binders =
+let intern_context global_level env impl_env binders =
   try
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let lenv, bl = List.fold_left
-	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar)
+	    (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map snd bl)
@@ -1869,7 +1868,7 @@ let interp_rawcontext_evars evdref env bl =
   in (env, par), impls
 
 let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
-  let int_env,bl = intern_context global_level !evdref env impl_env params in
+  let int_env,bl = intern_context global_level env impl_env params in
   let x = interp_rawcontext_evars evdref env bl in
   int_env, x
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index a4f3e057fd..bbee249572 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -74,18 +74,18 @@ type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
 (** {6 Internalization performs interpretation of global names and notations } *)
 
-val intern_constr : evar_map -> env -> constr_expr -> glob_constr
+val intern_constr : env -> constr_expr -> glob_constr
 
-val intern_type : evar_map -> env -> constr_expr -> glob_constr
+val intern_type : env -> constr_expr -> glob_constr
 
-val intern_gen : typing_constraint -> evar_map -> env ->
+val intern_gen : typing_constraint -> env ->
   ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
   Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
+val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -132,7 +132,7 @@ val interp_type_evars_impls : evar_map ref -> env ->
 (** Interprets constr patterns *)
 
 val intern_constr_pattern :
-  evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
+  env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d1bc28333b..fef32a5ff9 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -15,7 +15,6 @@ open Genarg
 type glob_sign = {
   ltacvars : Id.Set.t;
   ltacrecvars : Nametab.ltac_constant Id.Map.t;
-  gsigma : Evd.evar_map;
   genv : Environ.env }
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 7027315e76..970f27f66a 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -13,7 +13,6 @@ open Genarg
 type glob_sign = {
   ltacvars : Id.Set.t;
   ltacrecvars : Nametab.ltac_constant Id.Map.t;
-  gsigma : Evd.evar_map;
   genv : Environ.env }
 
 (** {5 Internalization functions} *)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b21037d252..6e53ae6a21 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1456,8 +1456,7 @@ let do_instr raw_instr pts =
             let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma; } in
       let env=  pf_env gl in
-      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
-		 gsigma = sigma; genv = env} in
+      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dc59b7ca7..661e5e4869 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function
         (abstract_glob_constr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
-  Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls
+  Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
     ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty) c
 
 (*
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b7c471f4ae..ac54e44cc7 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -71,7 +71,7 @@ let isVarf f x =
 let ident_global_exist id =
   try
     let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
-    let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
+    let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when Errors.noncritical e -> false
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 36ba80202f..8c27767898 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -63,7 +63,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
 let instantiate_pf_com evk com sigma =
   let evi = Evd.find sigma evk in
   let env = Evd.evar_filtered_env evi in
-  let rawc = Constrintern.intern_constr sigma env com in
+  let rawc = Constrintern.intern_constr env com in
   let ltac_vars = (Id.Map.empty, Id.Map.empty) in
   let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
   sigma'
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9156e1f04d..fc9a335e68 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -859,7 +859,7 @@ let interp_hints =
     let path, gr = fi c in
       (o, b, path, gr)
   in
-  let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
+  let fp = Constrintern.intern_constr_pattern (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
   | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 59bad5808a..7f676c157a 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -57,12 +57,10 @@ type glob_sign = Genintern.glob_sign = {
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
   ltacrecvars : ltac_constant Id.Map.t;
      (* ltac recursive names *)
-  gsigma : Evd.evar_map;
   genv : Environ.env }
 
 let fully_empty_glob_sign =
-  { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
-    gsigma = Evd.empty; genv = Environ.empty_env }
+  { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env }
 
 let make_empty_glob_sign () =
   { fully_empty_glob_sign with genv = Global.env () }
@@ -252,12 +250,12 @@ let intern_binding_name ist x =
      and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
   let ltacvars = (lfun, Id.Set.empty) in
   let c' =
-    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
+    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
   in
   (c',if !strict_check then None else Some c)
 
@@ -330,7 +328,7 @@ let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 let intern_constr_pattern ist ~as_type ~ltacvars pc =
   let ltacvars = ltacvars, Id.Set.empty in
   let metas,pat = Constrintern.intern_constr_pattern
-    ist.gsigma ist.genv ~as_type ~ltacvars pc
+    ist.genv ~as_type ~ltacvars pc
   in
   let c = intern_constr_gen true false ist pc in
   metas,(c,pat)
@@ -701,7 +699,7 @@ and intern_match_rule onlytac ist = function
   | (All tc)::tl ->
       All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
   | (Pat (rl,mp,tc))::tl ->
-      let {ltacvars=lfun; gsigma=sigma; genv=env} = ist in
+      let {ltacvars=lfun; genv=env} = ist in
       let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
       let ido,metas2,pat = intern_pattern ist lfun mp in
       let fold accu x = Id.Set.add x accu in
@@ -760,7 +758,7 @@ let glob_tactic_env l env x =
     List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
   (intern_pure_tactic
-    { ltacvars; ltacrecvars = Id.Map.empty; gsigma = Evd.empty; genv = env })
+    { ltacvars; ltacrecvars = Id.Map.empty; genv = env })
     x
 
 let split_ltac_fun = function
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index c04b6f3912..8473f585bd 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -26,7 +26,6 @@ open Nametab
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
   ltacrecvars : ltac_constant Id.Map.t;
-  gsigma : Evd.evar_map;
   genv : Environ.env }
 
 val fully_empty_glob_sign : glob_sign
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2e54653403..433322e4c1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -485,7 +485,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       let ltacvars = Id.Map.domain constrvars in
       let bndvars = Id.Map.domain ist.lfun in
       let ltacdata = (ltacvars, bndvars) in
-      intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
+      intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
@@ -2078,8 +2078,7 @@ let eval_tactic_ist ist t =
 
 let interp_tac_gen lfun avoid_ids debug t =
   Proofview.Goal.enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
   let ist = { lfun = lfun; extra = extra } in
@@ -2087,7 +2086,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   interp_tactic ist
     (intern_pure_tactic {
       ltacvars; ltacrecvars = Id.Map.empty;
-      gsigma = sigma; genv = env } t)
+      genv = env } t)
   end
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -2101,9 +2100,9 @@ let eval_ltac_constr t =
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
-  let hide_interp env sigma =
+  let hide_interp env =
     let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
-                gsigma = sigma; genv = env } in
+                genv = env } in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with
@@ -2112,11 +2111,10 @@ let hide_interp global t ot =
   in
   if global then
     Proofview.tclENV >= fun env ->
-    Proofview.tclEVARMAP >= fun sigma ->
-    hide_interp env sigma
+    hide_interp env
   else
     Proofview.Goal.enter begin fun gl ->
-      hide_interp (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+      hide_interp (Proofview.Goal.env gl)
     end
 
 (***************************************************************************)
@@ -2170,7 +2168,7 @@ let () =
 
 let interp_redexp env sigma r =
   let ist = default_ist () in
-  let gist = { fully_empty_glob_sign with genv = env; gsigma = sigma } in
+  let gist = { fully_empty_glob_sign with genv = env; } in
   interp_red_expr ist sigma env (intern_red_expr gist r)
 
 (***************************************************************************)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9e61bc7fb7..91762c0003 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -247,11 +247,11 @@ let interface_search flags =
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
   | (Interface.Type_Pattern s, b) :: l ->
     let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    let (_, pat) = Constrintern.intern_constr_pattern env constr in
     extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
   | (Interface.SubType_Pattern s, b) :: l ->
     let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    let (_, pat) = Constrintern.intern_constr_pattern env constr in
     extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
   | (Interface.In_Module m, b) :: l ->
     let path = String.concat "." m in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index db51ff6103..399471b74a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1431,7 +1431,7 @@ open Search
 
 let interp_search_about_item = function
   | SearchSubPattern pat ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in
+      let _,pat = intern_constr_pattern (Global.env()) pat in
       GlobSearchSubPattern pat
   | SearchString (s,None) when Id.is_valid s ->
       GlobSearchString s
@@ -1448,7 +1448,7 @@ let interp_search_about_item = function
 let vernac_search s r =
   let r = interp_search_restriction r in
   let env = Global.env () in
-  let get_pattern c = snd (Constrintern.intern_constr_pattern Evd.empty env c) in
+  let get_pattern c = snd (Constrintern.intern_constr_pattern env c) in
   match s with
   | SearchPattern c ->
       msg_notice (Search.search_pattern (get_pattern c) r)