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.

9 files changed, 58 insertions, 73 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d6ed201d8..79d2e4694 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -25,7 +25,6 @@ open Pretype_errors
 open Evarutil
 open Unification
 open Misctypes
-open Sigma.Notations
 
 (******************************************************************)
 (* Clausal environments *)
@@ -337,9 +336,8 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
-        let evd = Sigma.Unsafe.of_evar_map clenv.evd in
-	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
-	let evd = Sigma.to_evar_map evd in
+        let evd = clenv.evd in
+	let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
@@ -614,9 +612,7 @@ let make_evar_clause env sigma ?len t =
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
-      let sigma = Sigma.to_evar_map sigma in
+      let (sigma, ev) = new_evar ~store env sigma t1 in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 4bcd50591..f43c0531d 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -41,10 +41,10 @@ val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
-  ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
+  'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
@@ -66,7 +66,7 @@ val old_clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
 val clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+  ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv
 
 val clenv_dependent : clausenv -> metavariable list
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 0722ea047..2ce144a6d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -17,7 +17,6 @@ open Logic
 open Reduction
 open Tacmach
 open Clenv
-open Proofview.Notations
 
 (* This function put casts around metavariables whose type could not be
  * infered by the refiner, that is head of applications, predicates and
@@ -104,10 +103,10 @@ open Unification
 let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let clenv = clenv_unique_resolver ~flags clenv gl in
     clenv_refine with_evars ~with_classes clenv
-  end }
+  end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
@@ -139,7 +138,7 @@ let fail_quick_unif_flags = {
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unify ?(flags=fail_quick_unif_flags) m =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
     let evd = clear_metas (Tacmach.New.project gl) in
@@ -147,4 +146,4 @@ let unify ?(flags=fail_quick_unif_flags) m =
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when CErrors.noncritical e -> Proofview.tclZERO e
-  end }
+  end
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 5a717f166..e69ef18fd 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Pp
-open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
 
@@ -73,9 +72,7 @@ module V82 = struct
 		Evd.evar_extra = extra }
     in
     let evi = Typeclasses.mark_unresolvable evi in
-    let evars = Sigma.Unsafe.of_evar_map evars in
-    let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in
-    let evars = Sigma.to_evar_map evars in
+    let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
@@ -131,9 +128,7 @@ module V82 = struct
     let new_evi =
       { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in
-    let sigma = Sigma.Unsafe.of_evar_map Evd.empty in
-    let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in
-    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
     { Evd.it = evk ; sigma = sigma; }
 
   (* Used by the compatibility layer and typeclasses *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 383a6a523..458dd2161 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -201,7 +201,7 @@ let out_arg = function
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
+let e_red f env evm c = evm, f env evm c
 
 let head_style = false (* Turn to true to have a semantics where simpl
    only reduce at the head when an evaluable reference is given, e.g.
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 63ae41075..caa6b9fb3 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Util
-open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
@@ -73,7 +72,6 @@ let add_side_effects env effects =
 let generic_refine ?(unsafe = true) f gl =
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
-  let sigma = Sigma.to_evar_map sigma in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   (** Save the [future_goals] state to restore them after the
@@ -129,19 +127,20 @@ let generic_refine ?(unsafe = true) f gl =
 let lift c =
   Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.V82.wrap_exceptions begin fun () ->
-  let Sigma (c, sigma, _) = c.run (Sigma.Unsafe.of_evar_map sigma) in
-  Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () ->
+  let (sigma, c) = c sigma in
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
   Proofview.tclUNIT c
   end
 
-let make_refine_enter ?unsafe f =
-  { enter = fun gl -> generic_refine ?unsafe (lift f) gl }
+let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl
 
 let refine_one ?(unsafe = true) f =
   Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
 
 let refine ?(unsafe = true) f =
-  let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in
+  let f evd =
+    let (evd,c) = f evd in (evd,((), c))
+  in
   Proofview.Goal.enter (make_refine_enter ~unsafe f)
 
 (** Useful definitions *)
@@ -154,17 +153,16 @@ let with_type env evd c t =
   in
   evd , j'.Environ.uj_val
 
-let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
+let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl ->
   let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
-  let f = { run = fun h ->
-    let Sigma (c, h, p) = f.run h in
-    let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
-    Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
-  } in
+  let f h =
+    let (h, c) = f h in
+    with_type env h c concl
+  in
   refine ?unsafe f
-end }
+end
 
 (** {7 solve_constraints}
 
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 5098f246a..f1439f9a1 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,7 +21,7 @@ val pr_constr :
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
+val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
 (** In [refine ?unsafe t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
@@ -30,11 +30,11 @@ val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
     tactic failures. If [unsafe] is [false] (default is [true]) [t] is
     type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
+val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
 (** A variant of [refine] which assumes exactly one goal under focus *)
 
 val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
-  ([ `NF ], 'r) Proofview.Goal.t -> 'a tactic
+  [ `NF ] Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
 
 (** {7 Helper functions} *)
@@ -44,7 +44,7 @@ val with_type : Environ.env -> Evd.evar_map ->
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
+val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
 
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
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 1172e55ac..3d2fa72c1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -99,47 +99,47 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
-  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference
+  val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
+  val pf_global : identifier -> 'a Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
 
-  val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
-  val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
-  val pf_concl : ('a, 'r) Proofview.Goal.t -> types
+  val project : 'a Proofview.Goal.t -> Evd.evar_map
+  val pf_env : 'a Proofview.Goal.t -> Environ.env
+  val pf_concl : 'a Proofview.Goal.t -> types
 
   (** WRONG: To be avoided at all costs, it typechecks the term entirely but
      forgets the universe constraints necessary to retypecheck it *)
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types
 
   (** This function does no type inference and expects an already well-typed term.
       It recomputes its type in the fastest way possible (no conversion is ever involved) *)
-  val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types
 
   (** This function entirely type-checks the term and computes its type
       and the implied universe constraints. *)
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types
-  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool
+  val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types
+  val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool
 
-  val pf_get_new_id  : identifier -> ('a, 'r) Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
-  val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
+  val pf_get_new_id  : identifier -> 'a Proofview.Goal.t -> identifier
+  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
 
-  val pf_get_hyp : identifier -> ('a, 'r) Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : identifier -> ('a, 'r) Proofview.Goal.t -> types
-  val pf_last_hyp           : ('a, 'r) Proofview.Goal.t -> named_declaration
+  val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : identifier -> 'a Proofview.Goal.t -> types
+  val pf_last_hyp           : 'a Proofview.Goal.t -> named_declaration
 
-  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
+  val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
 
-  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
-  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
 
-  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
-  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
+  val pf_compute : 'a Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
 
-  val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
 
 end