Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.

1 files changed, 68 insertions, 72 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 94f22f903..27c1987a0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -267,40 +267,6 @@ let pf_with_evars glsev k gls =
 let pf_constr_of_global gr k =
   pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
 
-(* computing the case/elim combinators *)
-
-let gl_make_elim ind gl =
-  let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
-  let (sigma, c) = pf_apply Evd.fresh_global gl gr in
-  (sigma, EConstr.of_constr c)
-
-let gl_make_case_dep ind gl =
-  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
-  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
-    (elimination_sort_of_goal gl)
-  in
-  (Sigma.to_evar_map sigma, EConstr.of_constr r)
-
-let gl_make_case_nodep ind gl =
-  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
-  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
-    (elimination_sort_of_goal gl)
-  in
-  (Sigma.to_evar_map sigma, EConstr.of_constr r)
-
-let make_elim_branch_assumptions ba gl =
-  let assums =
-    try List.rev (List.firstn ba.nassums (pf_hyps gl))
-    with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
-  { ba = ba; assums = assums }
-
-let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
-
-let make_case_branch_assumptions = make_elim_branch_assumptions
-
-let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
-
-
 (** Tacticals of Ltac defined directly in term of Proofview *)
 module New = struct
   open Proofview
@@ -534,7 +500,7 @@ module New = struct
         Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclDELAYEDWITHHOLES check x tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
       let Sigma (x, sigma, _) = x.delayed env sigma in
@@ -578,13 +544,13 @@ module New = struct
   let onLastHyp   = onNthHyp 1
 
   let onNthDecl m tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       Proofview.tclUNIT (nthDecl m gl) >>= tac
     end }
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
     if pred (id,typ) then
       tac1 id
@@ -592,7 +558,7 @@ module New = struct
       tac2 id
     end }
 
-  let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
+  let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end }
 
   let afterHyp id tac =
     Proofview.Goal.enter { enter = begin fun gl ->
@@ -625,13 +591,13 @@ module New = struct
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
       isrec allnames tac predicate ind (c, t) =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let sigma, elim = (mk_elim ind).enter gl in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
+    (Proofview.Goal.enter { enter = begin fun gl ->
+    let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
+    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
     let indmv =
       match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
@@ -660,7 +626,7 @@ module New = struct
       | None   -> elimclause'
       | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
     in
-    let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
+    let clenv' = clenv_unique_resolver ~flags elimclause' gl in
     let after_tac i =
       let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in
       let ba = { branchsign = branchsigns.(i);
@@ -679,8 +645,64 @@ module New = struct
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end }) end }
 
+  let elimination_sort_of_goal gl =
+    (** Retyping will expand evars anyway. *)
+    let c = Proofview.Goal.concl (Goal.assume gl) in
+    pf_apply Retyping.get_sort_family_of gl c
+
+  let elimination_sort_of_hyp id gl =
+    (** Retyping will expand evars anyway. *)
+    let c = pf_get_hyp_typ id (Goal.assume gl) in
+    pf_apply Retyping.get_sort_family_of gl c
+
+  let elimination_sort_of_clause id gl = match id with
+  | None -> elimination_sort_of_goal gl
+  | Some id -> elimination_sort_of_hyp id gl
+
+  (* computing the case/elim combinators *)
+
+  let gl_make_elim ind = { enter = begin fun gl ->
+    let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
+    let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+    (sigma, EConstr.of_constr c)
+  end }
+
+  let gl_make_case_dep ind = { enter = begin fun gl ->
+    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
+      (elimination_sort_of_goal gl)
+    in
+    (Sigma.to_evar_map sigma, EConstr.of_constr r)
+  end }
+
+  let gl_make_case_nodep ind = { enter = begin fun gl ->
+    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
+      (elimination_sort_of_goal gl)
+    in
+    (Sigma.to_evar_map sigma, EConstr.of_constr r)
+  end }
+
+  let make_elim_branch_assumptions ba hyps =
+    let assums =
+      try List.rev (List.firstn ba.nassums hyps)
+      with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+    { ba = ba; assums = assums }
+
+  let elim_on_ba tac ba =
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+    tac branches
+    end }
+
+  let case_on_ba tac ba = 
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+    tac branches
+    end }
+
   let elimination_then tac c =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
     let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
@@ -696,34 +718,8 @@ module New = struct
   let case_nodep_then_using =
     general_elim_then_using gl_make_case_nodep false
 
-  let elim_on_ba tac ba =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
-    tac branches
-    end }
-
-  let case_on_ba tac ba = 
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
-    tac branches
-    end }
-
-  let elimination_sort_of_goal gl =
-    (** Retyping will expand evars anyway. *)
-    let c = Proofview.Goal.concl (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
-
-  let elimination_sort_of_hyp id gl =
-    (** Retyping will expand evars anyway. *)
-    let c = pf_get_hyp_typ id (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
-
-  let elimination_sort_of_clause id gl = match id with
-  | None -> elimination_sort_of_goal gl
-  | Some id -> elimination_sort_of_hyp id gl
-
   let pf_constr_of_global ref tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Tacmach.New.project gl in
       let (sigma, c) = Evd.fresh_global env sigma ref in