Merge branch 'trunk' of github.com:coq/coq into trunk

14 files changed, 47 insertions, 56 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0a2a459d3..e9ebcf39f 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 a4f3e057f..bbee24957 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 d1bc28333..fef32a5ff 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 7027315e7..970f27f66 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 b21037d25..6e53ae6a2 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 3dc59b7ca..661e5e486 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 b7c471f4a..ac54e44cc 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 36ba80202..8c2776789 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 9156e1f04..fc9a335e6 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 59bad5808..7f676c157 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 c04b6f391..8473f585b 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 2e5465340..433322e4c 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 9e61bc7fb..91762c000 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 db51ff610..399471b74 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)