1 files changed, 42 insertions, 43 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a7eadc3c3..aa574e41c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -17,7 +17,6 @@ open Declarations
 open Tacmach
 open Clenv
 open Tactypes
-open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
 
@@ -511,12 +510,12 @@ module New = struct
         Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclDELAYEDWITHHOLES check x tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.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
-      tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
-    end }
+      let (sigma, x) = x env sigma in
+      tclWITHHOLES check (tac x) sigma
+    end
 
   let tclTIMEOUT n t =
     Proofview.tclOR
@@ -547,66 +546,66 @@ module New = struct
     mkVar (nthHypId m gl)
 
   let onNthHypId m tac =
-    Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end }
+    Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end 
   let onNthHyp m tac =
-    Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end }
+    Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
 
   let onLastHypId = onNthHypId 1
   let onLastHyp   = onNthHyp 1
 
   let onNthDecl m tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       Proofview.tclUNIT (nthDecl m gl) >>= tac
-    end }
+    end
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
     if pred (id,typ) then
       tac1 id
     else
       tac2 id
-    end }
+    end
 
-  let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end }
+  let onHyps find tac = Proofview.Goal.enter begin fun gl -> tac (find gl) end
 
   let afterHyp id tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
     tac rem
-    end }
+    end
 
   let fullGoal gl =
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     None :: List.map Option.make hyps
 
   let tryAllHyps tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclFIRST_PROGRESS_ON tac hyps
-    end }
+    end
   let tryAllHypsAndConcl tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       tclFIRST_PROGRESS_ON tac (fullGoal gl)
-    end }
+    end
 
   let onClause tac cl =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
-    end }
+    end
 
   (* Find the right elimination suffix corresponding to the sort of the goal *)
   (* 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.enter { enter = begin fun gl ->
-    let sigma, elim = (mk_elim ind).enter gl in
+    Proofview.Goal.enter begin fun gl ->
+    let sigma, elim = mk_elim ind gl in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Proofview.Goal.enter { enter = begin fun gl ->
+    (Proofview.Goal.enter begin fun gl ->
     let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
     let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
@@ -655,7 +654,7 @@ module New = struct
     Proofview.tclTHEN
       (Clenvtac.clenv_refine false clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
-    end }) end }
+    end) end
 
   let elimination_sort_of_goal gl =
     (** Retyping will expand evars anyway. *)
@@ -673,29 +672,29 @@ module New = struct
 
   (* computing the case/elim combinators *)
 
-  let gl_make_elim ind = { enter = begin fun gl ->
+  let gl_make_elim ind = 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 }
+  end
 
-  let gl_make_case_dep (ind, u) = { enter = begin fun gl ->
-    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+  let gl_make_case_dep (ind, u) = begin fun gl ->
+    let sigma = project gl in
     let u = EInstance.kind (project gl) u in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
+    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
       (elimination_sort_of_goal gl)
     in
-    (Sigma.to_evar_map sigma, EConstr.of_constr r)
-  end }
+    (sigma, EConstr.of_constr r)
+  end
 
-  let gl_make_case_nodep (ind, u) = { enter = begin fun gl ->
-    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
-    let u = EInstance.kind (project gl) u in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
+  let gl_make_case_nodep (ind, u) = begin fun gl ->
+    let sigma = project gl in
+    let u = EInstance.kind sigma u in
+    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
       (elimination_sort_of_goal gl)
     in
-    (Sigma.to_evar_map sigma, EConstr.of_constr r)
-  end }
+    (sigma, EConstr.of_constr r)
+  end
 
   let make_elim_branch_assumptions ba hyps =
     let assums =
@@ -704,19 +703,19 @@ module New = struct
     { ba = ba; assums = assums }
 
   let elim_on_ba tac ba =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
     tac branches
-    end }
+    end
 
   let case_on_ba tac ba = 
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
     tac branches
-    end }
+    end
 
   let elimination_then tac c =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.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
@@ -724,7 +723,7 @@ module New = struct
       | Some _ -> false,gl_make_case_dep
     in
     general_elim_then_using mkelim isrec None tac None ind (c, t)
-    end }
+    end
 
   let case_then_using =
     general_elim_then_using gl_make_case_dep false