Remove the Sigma (monotonous state) API.

Reminder of (some of) the reasons for removal:

- Despite the claim in sigma.mli, it does *not* prevent evar
  leaks, something like:

  fun env evd ->
  let (evd',ev) = new_evar env evd in
  (evd,ev)

  will typecheck even with Sigma-like type annotations (with a proof of
  reflexivity)

- The API stayed embryonic. Even typing functions were not ported to
  Sigma.

- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
  less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
  at all (despite still being so).

- There was no good story for higher order functions manipulating evar
  maps. Without higher order, one can most of the time get away with
  reusing the same name for the updated evar map.

- Most of the code doing complex things with evar maps was using unsafe
  casts to sigma. This code should be fixed, but this is an orthogonal
  issue.

Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.

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