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, 14 deletions

diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index a11619846..2d86daadb 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -17,15 +17,9 @@ open Namegen
 open Evd
 open Evarutil
 open Pretype_errors
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  (Sigma.to_evar_map evd, evk)
-
 let env_nf_evar sigma env =
   let nf_evar c = nf_evar sigma c in
   process_rel_context
@@ -82,9 +76,7 @@ let define_pure_evar_as_product evd evk =
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
-    let evd = Sigma.Unsafe.of_evar_map evd in
-    let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
-    (Sigma.to_evar_map evd1, e)
+    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi)
   in
   let evd2,rng =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
@@ -92,13 +84,11 @@ let define_pure_evar_as_product evd evk =
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
-        new_evar_unsafe newenv evd1 concl ~src ~filter
+        new_evar newenv evd1 concl ~src ~filter
       else
 	let status = univ_flexible_alg in
 	let evd3, (rng, srng) =
-          let evd1 = Sigma.Unsafe.of_evar_map evd1 in
-          let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
-          (Sigma.to_evar_map evd3, e)
+          new_type_evar newenv evd1 status ~src ~filter
         in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in
@@ -143,7 +133,7 @@ let define_pure_evar_as_lambda env evd evk =
   let newenv = push_named (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
-  let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam