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, 4 insertions, 7 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 66d91c634..f9d9f25cc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -18,7 +18,6 @@ open Tacred
 open Proof_type
 open Logic
 open Refiner
-open Sigma.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -79,9 +78,8 @@ let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrinte
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
-  let sigma = Sigma.Unsafe.of_evar_map (project gls) in
-  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
-  (Sigma.to_evar_map sigma, c)
+  let sigma = project gls in
+  redfun (pf_env gls) sigma c
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
@@ -158,8 +156,7 @@ let pr_glls glls =
 module New = struct
 
   let project gl =
-    let sigma = Proofview.Goal.sigma gl in
-    Sigma.to_evar_map sigma
+    Proofview.Goal.sigma gl
 
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (project gl)
@@ -216,7 +213,7 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
-  let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) =
+  let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) =
     (** We normalize the conclusion just after *)
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in