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.

4 files changed, 15 insertions, 20 deletions

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)
 
 (***************************************************************************)