Removing the evar_map argument from s_enter.

8 files changed, 46 insertions, 25 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4a520612f..4fb4b3263 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -119,7 +119,8 @@ let exact poly (c,clenv) =
       let ctx = Evd.evar_universe_context clenv.evd in
 	ctx, c
   in
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let sigma = Sigma.to_evar_map sigma in
     let sigma = Evd.merge_universe_context sigma ctx in
     Sigma.Unsafe.of_pair (exact_check c', sigma)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 43a8d7f06..e4ff1c906 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -94,7 +94,8 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tac
 let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = find_rewrites bas in
   let try_rewrite dir ctx c tc =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
     let sigma = Sigma.to_evar_map sigma in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0cc74ff44..5ccf4a9e4 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -24,7 +24,8 @@ let mk_absurd_proof t =
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
     let j = Retyping.get_judgment_of env sigma c in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 56878f112..2edd67ef8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -347,7 +347,7 @@ let type_of_clause cls gl = match cls with
   | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
@@ -1483,7 +1483,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index c9fc01088..4c4d74503 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -70,7 +70,8 @@ let instantiate_tac_by_name id c =
 
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let id = match name with
     | Names.Anonymous -> 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e1997c705..5201d54d6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -618,7 +618,8 @@ let out_arg = function
   | ArgArg x -> x
 
 let hResolve id c occ t =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a9fa52e92..ed1a62795 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -432,7 +432,8 @@ let rewrite_equations_tac as_mode othin id neqns names ba =
     tac
 
 let raw_inversion inv_kind id status names =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let sigma = Sigma.to_evar_map sigma in
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 65d2749b5..62f306927 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -610,7 +610,8 @@ let e_reduct_option ?(check=false) redfun = function
     from conversions. *)
 
 let e_change_in_concl (redfun,sty) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let sigma = Sigma.to_evar_map sigma in
     let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in
     Sigma.Unsafe.of_pair (convert_concl_no_check c sty, sigma)
@@ -633,7 +634,8 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
 	sigma', (id,Some b',ty')
 
 let e_change_in_hyp redfun (id,where) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let sigma = Sigma.to_evar_map sigma in
     let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
     let sigma, c = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
@@ -1247,7 +1249,8 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
 (* Case analysis tactics *)
 
 let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
@@ -1297,7 +1300,7 @@ let find_eliminator c gl =
 
 let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
-    (Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+    (Proofview.Goal.s_enter { s_enter = begin fun gl ->
       let sigma, elim = find_eliminator c gl in
       let tac =
 	  (general_elim with_evars clear_flag cx elim)
@@ -1469,7 +1472,8 @@ let descend_in_conjunctions avoid tac (err, info) c =
 (****************************************************)
 
 let solve_remaining_apply_goals =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   if !apply_solve_class_goals then
     try 
       let env = Proofview.Goal.env gl in
@@ -1736,7 +1740,8 @@ let new_exact_no_check c =
   Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
 
 let exact_check c =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   (** We do not need to normalize the goal because we just check convertibility *)
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   let env = Proofview.Goal.env gl in
@@ -1952,7 +1957,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if i > nconstr then error "Not enough constructors."
 
 let constructor_tac with_evars expctdnumopt i lbind =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let cl = Tacmach.New.pf_nf_concl gl in
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
@@ -2371,7 +2377,8 @@ let decode_hyp = function
 *)
 
 let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let t = match ty with Some t -> t | _ -> typ_of env sigma c in
     let Sigma ((newcl, eq_tac), sigma, p) = match with_eq with
@@ -2447,7 +2454,8 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       Sigma (mkNamedLetIn id c t x, sigma, p)
 
 let letin_tac with_eq id c ty occs =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
     let abs = AbstractExact (id,c,ty,occs,true) in
@@ -2458,7 +2466,8 @@ let letin_tac with_eq id c ty occs =
   end }
 
 let letin_pat_tac with_eq id c occs =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
     let check t = true in
@@ -2616,7 +2625,8 @@ let generalize_gen_let lconstr gl =
       if Option.is_empty b then Some c else None) lconstr)) gl
 
 let new_generalize_gen_let lconstr =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Sigma.to_evar_map sigma in
@@ -3794,7 +3804,8 @@ let induction_tac with_evars params indvars elim gl =
    induction applies with the induction hypotheses *)
 
 let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
     let concl = Tacmach.New.pf_nf_concl gl in
@@ -3961,7 +3972,8 @@ let check_enough_applied env sigma elim =
 
 let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
      id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let ccl = Proofview.Goal.raw_concl gl in
   let store = Proofview.Goal.extra gl in
@@ -4247,14 +4259,15 @@ let elim_scheme_type elim t =
   end }
 
 let elim_type t =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
   let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
   Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd)
   end }
 
 let case_type t =
-  Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let env = Tacmach.New.pf_env gl in
   let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
   let s = Tacticals.New.elimination_sort_of_goal gl in
@@ -4512,7 +4525,8 @@ let abstract_subproof id gk tac =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let current_sign = Global.named_context()
   and global_sign = Proofview.Goal.hyps gl in
   let sigma = Sigma.to_evar_map sigma in
@@ -4591,7 +4605,8 @@ let tclABSTRACT name_op tac =
   abstract_subproof s gk tac
 
 let unify ?(state=full_transparent_state) x y =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   try
     let core_flags =
       { (default_unify_flags ()).core_unify_flags with