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.

11 files changed, 63 insertions, 418 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 33d7acc31..078f2fc33 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -780,9 +780,8 @@ let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
 let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
 
 let fresh_global ?loc ?rigid ?names env sigma reference =
-  let Sigma.Sigma (t,sigma,p) =
-    Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
-  Sigma.Sigma (of_constr t,sigma,p)
+  let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
+  evd, of_constr t
 
 let is_global sigma gr c =
   Globnames.is_global gr (to_constr sigma c)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 94b7ca96a..07a4dc8e2 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -259,7 +259,7 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
-  'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
+  Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t
 
 val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
 
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 1b670d366..afc02d7f6 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -2,7 +2,6 @@ Logic_monad
 Universes
 UState
 Evd
-Sigma
 EConstr
 Namegen
 Termops
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 59ad4ef47..e8d184632 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -15,7 +15,6 @@ open Namegen
 open Pre_env
 open Environ
 open Evd
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -45,8 +44,8 @@ let e_new_global evdref x =
   EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x)
 
 let new_global evd x = 
-  let Sigma (c, sigma, p) = Sigma.fresh_global (Global.env()) evd x in
-  Sigma (EConstr.of_constr c, sigma, p)
+  let (evd, c) = Evd.fresh_global (Global.env()) evd x in
+  (evd, EConstr.of_constr c)
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
@@ -368,20 +367,17 @@ let push_rel_context_to_named_context env sigma typ =
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
 let restrict_evar evd evk filter ?src candidates =
-  let evd = Sigma.to_evar_map evd in
   let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
-  Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
+  Evd.declare_future_goal evk' evd, evk'
 
 let new_pure_evar_full evd evi =
-  let evd = Sigma.to_evar_map evd in
   let (evd, evk) = Evd.new_evar evd evi in
   let evd = Evd.declare_future_goal evk evd in
-  Sigma.Unsafe.of_pair (evk, evd)
+  (evd, evk)
 
 let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
   let typ = EConstr.Unsafe.to_constr typ in
-  let evd = Sigma.to_evar_map evd in
   let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
@@ -407,19 +403,19 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
   in
-  Sigma.Unsafe.of_pair (newevk, evd)
+  (evd, newevk)
 
 let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  evd, mkEvar (newevk,Array.of_list instance)
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env (Sigma.to_evar_map evd) typ in
+  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env evd typ in
   let map c = subst2 subst vsubst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
@@ -428,27 +424,20 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-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 new_type_evar env evd ?src ?filter ?naming ?principal rigid =
-  let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
-  let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in
-  Sigma ((e, s), evd', p +> q)
+  let (evd', s) = new_sort_variable rigid evd in
+  let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in
+  evd', (e, s)
 
 let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
-  let sigma = Sigma.Unsafe.of_evar_map !evdref in
-  let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
-  let sigma = Sigma.to_evar_map sigma in
-    evdref := sigma;
+  let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
+    evdref := evd;
     c
 
 let new_Type ?(rigid=Evd.univ_flexible) env evd = 
   let open EConstr in
-  let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
-  Sigma (mkSort s, sigma, p)
+  let (evd, s) = new_sort_variable rigid evd in
+  (evd, mkSort s)
 
 let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
   let evd', s = new_sort_variable rigid !evdref in
@@ -456,7 +445,7 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
 
   (* The same using side-effect *)
 let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
-  let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
+  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
   evdref := evd';
   ev
 
@@ -552,9 +541,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
             else
               let origfilter = Evd.evar_filter evi in
               let filter = Evd.Filter.apply_subfilter origfilter filter in
-              let evd = Sigma.Unsafe.of_evar_map !evdref in
-              let Sigma (_, evd, _) = restrict_evar evd evk filter None in
-              let evd = Sigma.to_evar_map evd in
+              let evd = !evdref in
+              let (evd,_) = restrict_evar evd evk filter None in
               evdref := evd;
 	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
 	      let evi = Evd.find !evdref evk in
@@ -723,8 +711,8 @@ let occur_evar_upto sigma n c =
 
 let judge_of_new_Type evd =
   let open EConstr in
-  let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
-  Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
+  let (evd', s) = new_univ_variable univ_rigid evd in
+  (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) })
 
 let subterm_source evk (loc,k) =
   let evk = match k with
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 496ec5bc4..90c5c3dc0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -22,18 +22,18 @@ val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> (constr, 'r) Sigma.sigma
+  ?principal:bool -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
-  named_context_val -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
+  ?principal:bool -> types -> evar_map * evar
 
-val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
+val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 
 (** the same with side-effects *)
 val e_new_evar :
@@ -45,23 +45,23 @@ val e_new_evar :
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  (constr * sorts, 'r) Sigma.sigma
+  evar_map * (constr * sorts)
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
-val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
+val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
-val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
+val restrict_evar : evar_map -> existential_key -> Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * existential_key
 
 (** Polymorphic constants *)
 
-val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
+val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
 val e_new_global : evar_map ref -> Globnames.global_reference -> constr
 
 (** Create a fresh evar in a context different from its definition context:
@@ -71,11 +71,11 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> 'r Sigma.t -> types -> 
+ named_context_val -> evar_map -> types -> 
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
-  constr list -> (constr, 'r) Sigma.sigma
+  constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
 
@@ -133,7 +133,7 @@ val occur_evar_upto : evar_map -> Evar.t -> constr -> bool
 
 (** {6 Value/Type constraints} *)
 
-val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
+val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
 
 (***********************************************************)
 
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index aeaaea7e4..68368e38f 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -53,31 +53,17 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
   Proofview.tclUNIT (Depends filtered)
 
 let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-let set_sigma r =
-  let Sigma.Sigma (ans, sigma, _) = r in
-  Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () -> ans
 
 let nf_enter f =
   bind goals
     (fun gl ->
       gl >>= fun gl ->
       Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> f.enter nfgl))
-
-let nf_s_enter f =
-  bind goals
-    (fun gl ->
-      gl >>= fun gl ->
-      Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter nfgl)))
+      Proofview.V82.wrap_exceptions (fun () -> f nfgl))
 
 let enter f =
   bind goals
-    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f.enter gl))
-
-let s_enter f =
-  bind goals
-    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter gl)))
+    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
 
 let with_env t =
   t >>= function
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 5db373199..97bebe9da 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Proofview.Notations
-
 (** This module defines potentially focussing tactics. They are used by Ltac to
     emulate the historical behaviour of always-focussed tactics while still
     allowing to remain global when the goal is not needed. *)
@@ -41,20 +39,13 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 
 (** {5 Focussing} *)
 
-val nf_enter : ([ `NF ], 'a t) enter -> 'a t
+val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal. The resulting tactic is focussed. *)
 
-val enter : ([ `LZ ], 'a t) enter -> 'a t
+val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal, without evar normalization. The resulting tactic is
     focussed. *)
 
-val s_enter : ([ `LZ ], 'a t) s_enter -> 'a t
-(** Enter a goal and put back an evarmap. The resulting tactic is focussed. *)
-
-val nf_s_enter : ([ `NF ], 'a t) s_enter -> 'a t
-(** Enter a goal, without evar normalization and put back an evarmap. The
-    resulting tactic is focussed. *)
-
 val with_env : 'a t -> (Environ.env*'a) t
 (** [with_env t] returns, in addition to the return type of [t], an
     environment, which is the global environment if [t] does not focus on
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 29bb1ef39..39ef65dab 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -16,7 +16,6 @@
 open Pp
 open Util
 open Proofview_monad
-open Sigma.Notations
 open Context.Named.Declaration
 
 (** Main state of tactics *)
@@ -71,10 +70,8 @@ let dependent_init =
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
-    let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
-    let (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in
-    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in
+    let (gl, _) = EConstr.destEvar sigma econstr in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = gl :: comb; shelf = [] }
@@ -1012,20 +1009,17 @@ let catchable_exception = function
 
 module Goal = struct
 
-  type ('a, 'r) t = {
+  type 'a t = {
     env : Environ.env;
     sigma : Evd.evar_map;
     concl : EConstr.constr ;
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  type ('a, 'b) enter =
-    { enter : 'r. ('a, 'r) t -> 'b }
-
-  let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
+  let assume (gl : 'a t) = (gl :> [ `NF ] t)
 
   let env {env} = env
-  let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma
+  let sigma {sigma} = sigma
   let hyps {env} = EConstr.named_context env
   let concl {concl} = concl
   let extra {sigma; self} = goal_extra sigma self
@@ -1048,7 +1042,7 @@ module Goal = struct
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl))
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
       with e when catchable_exception e ->
         let (e, info) = CErrors.push e in
         tclZERO ~info e
@@ -1066,7 +1060,7 @@ module Goal = struct
     gmake_with info env sigma goal
 
   let enter f =
-    let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in
+    let f gl = InfoL.tag (Info.DBranch) (f gl) in
     InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
       Env.get >>= fun env ->
@@ -1091,48 +1085,13 @@ module Goal = struct
     | [goal] -> begin
        Env.get >>= fun env ->
        tclEVARMAP >>= fun sigma ->
-       try f.enter (gmake env sigma goal)
+       try f (gmake env sigma goal)
        with e when catchable_exception e ->
          let (e, info) = CErrors.push e in
          tclZERO ~info e
       end
     | _ -> tclZERO NotExactlyOneSubgoal
 
-  type ('a, 'b) s_enter =
-    { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
-
-  let s_enter f =
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try
-        let gl = gmake env sigma goal in
-        let Sigma (tac, sigma, _) = f.s_enter gl in
-        let sigma = Sigma.to_evar_map sigma in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
-      with e when catchable_exception e ->
-        let (e, info) = CErrors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  let nf_s_enter f =
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try
-        let (gl, sigma) = nf_gmake env sigma goal in
-        let Sigma (tac, sigma, _) = f.s_enter gl in
-        let sigma = Sigma.to_evar_map sigma in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
-      with e when catchable_exception e ->
-        let (e, info) = CErrors.push e in
-        tclZERO ~info e
-    end
-    end
-
   let goals =
     Pv.get >>= fun step ->
     let sigma = step.solution in
@@ -1156,8 +1115,6 @@ module Goal = struct
   (* compatibility *)
   let goal { self=self } = self
 
-  let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
-
 end
 
 
@@ -1281,8 +1238,4 @@ module Notations = struct
   let (>>=) = tclBIND
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-  type ('a, 'b) enter = ('a, 'b) Goal.enter =
-    { enter : 'r. ('a, 'r) Goal.t -> 'b }
-  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
-    { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma }
 end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index da8a8fecd..aae25b6f8 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -469,67 +469,48 @@ module Goal : sig
       data using {!assume} if you known you do not rely on the assumption of
       being normalized, at your own risk.
 
-      The second parameter is a stage indicating where the goal belongs. See
-      module {!Sigma}.
   *)
-  type ('a, 'r) t
+  type 'a t
 
   (** Assume that you do not need the goal to be normalized. *)
-  val assume : ('a, 'r) t -> ([ `NF ], 'r) t
+  val assume : 'a t -> [ `NF ] t
 
   (** Normalises the argument goal. *)
-  val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic
+  val normalize : 'a t -> [ `NF ] t tactic
 
   (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
       hypotheses) and the current evar map. *)
-  val concl : ('a, 'r) t -> constr
-  val hyps : ('a, 'r) t -> named_context
-  val env : ('a, 'r) t -> Environ.env
-  val sigma : ('a, 'r) t -> 'r Sigma.t
-  val extra : ('a, 'r) t -> Evd.Store.t
-
-  type ('a, 'b) enter =
-    { enter : 'r. ('a, 'r) t -> 'b }
+  val concl : 'a t -> constr
+  val hyps : 'a t -> named_context
+  val env : 'a t -> Environ.env
+  val sigma : 'a t -> Evd.evar_map
+  val extra : 'a t -> Evd.Store.t
 
   (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
       independently, in the manner of {!tclINDEPENDENT} except that
       the current goal is also given as an argument to [t]. The goal
       is normalised with respect to evars. *)
-  val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic
+  val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
 
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
-  val enter : ([ `LZ ], unit tactic) enter -> unit tactic
+  val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Like {!enter}, but assumes exactly one goal under focus, raising *)
   (** an error otherwise. *)
-  val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic
-
-  type ('a, 'b) s_enter =
-    { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
-
-  (** A variant of {!enter} allows to work with a monotonic state. The evarmap
-      returned by the argument is put back into the current state before firing
-      the returned tactic. *)
-  val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic
-
-  (** Like {!s_enter}, but normalizes the goal beforehand. *)
-  val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic
+  val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
       FIXME: encapsulate the level in an existential type. *)
-  val goals : ([ `LZ ], 'r) t tactic list tactic
+  val goals : [ `LZ ] t tactic list tactic
 
   (** [unsolved g] is [true] if [g] is still unsolved in the current
       proof state. *)
-  val unsolved : ('a, 'r) t -> bool tactic
+  val unsolved : 'a t -> bool tactic
 
   (** Compatibility: avoid if possible *)
-  val goal : ([ `NF ], 'r) t -> Evar.t
-
-  (** Every goal is valid at a later stage. FIXME: take a later evarmap *)
-  val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t
+  val goal : [ `NF ] t -> Evar.t
 
 end
 
@@ -616,8 +597,4 @@ module Notations : sig
   (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
 
-  type ('a, 'b) enter = ('a, 'b) Goal.enter =
-    { enter : 'r. ('a, 'r) Goal.t -> 'b }
-  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
-    { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma }
 end
diff --git a/engine/sigma.ml b/engine/sigma.ml
deleted file mode 100644
index 001f8be80..000000000
--- a/engine/sigma.ml
+++ /dev/null
@@ -1,117 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type 'a t = Evd.evar_map
-
-type ('a, 'b) le = unit
-
-let refl = ()
-let cons _ _  = ()
-let (+>) = fun _ _ -> ()
-
-type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
-
-type 'a evar = Evar.t
-
-let lift_evar evk () = evk
-
-let to_evar_map evd = evd
-let to_evar evk = evk
-
-let here x s = Sigma (x, s, ())
-
-(** API *)
-
-type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
-
-let new_evar sigma ?name info =
-  let (sigma, evk) = Evd.new_evar sigma ?name info in
-  Fresh (evk, sigma, ())
-
-let define evk c sigma =
-  Sigma ((), Evd.define evk c sigma, ())
-
-let new_univ_level_variable ?loc ?name rigid sigma =
-  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in
-  Sigma (u, sigma, ())
-
-let new_univ_variable ?loc ?name rigid sigma =
-  let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in
-  Sigma (u, sigma, ())
-
-let new_sort_variable ?loc ?name rigid sigma =
-  let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in
-  Sigma (u, sigma, ())
-
-let fresh_sort_in_family ?loc ?rigid env sigma s =
-  let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in
-  Sigma (s, sigma, ())
-
-let fresh_constant_instance ?loc env sigma cst =
-  let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in
-  Sigma (cst, sigma, ())
-
-let fresh_inductive_instance ?loc env sigma ind =
-  let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in
-  Sigma (ind, sigma, ())
-
-let fresh_constructor_instance ?loc env sigma pc =
-  let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in
-  Sigma (c, sigma, ())
-
-let fresh_global ?loc ?rigid ?names env sigma r =
-  let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in
-  Sigma (c, sigma, ())
-
-(** Run *)
-
-type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
-
-let run sigma f : 'a * Evd.evar_map =
-  let Sigma (x, sigma, ()) = f.run sigma in
-  (x, sigma)
-
-(** Monotonic references *)
-
-type evdref = Evd.evar_map ref
-
-let apply evdref f =
-  let Sigma (x, sigma, ()) = f.run !evdref in
-  evdref := sigma;
-  x
-
-let purify f =
-  let f (sigma : Evd.evar_map) =
-    let evdref = ref sigma in
-    let ans = f evdref in
-    Sigma (ans, !evdref, ())
-  in
-  { run = f }
-
-(** Unsafe primitives *)
-
-module Unsafe =
-struct
-
-let le = ()
-let of_evar_map sigma = sigma
-let of_evar evk = evk
-let of_ref ref = ref
-let of_pair (x, sigma) = Sigma (x, sigma, ())
-
-end
-
-module Notations =
-struct
-  type ('a, 'r) sigma_ = ('a, 'r) sigma =
-    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
-
-  let (+>) = fun _ _ -> ()
-
-  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
-end
diff --git a/engine/sigma.mli b/engine/sigma.mli
deleted file mode 100644
index 8e8df02f2..000000000
--- a/engine/sigma.mli
+++ /dev/null
@@ -1,131 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Constr
-
-(** Monotonous state enforced by typing.
-
-    This module allows to constrain uses of evarmaps in a monotonous fashion,
-    and in particular statically suppress evar leaks and the like. To this
-    ends, it defines a type of indexed evarmaps whose phantom typing ensures
-    monotonous use.
-*)
-
-(** {5 Stages} *)
-
-type ('a, 'b) le
-(** Relationship stating that stage ['a] is anterior to stage ['b] *)
-
-val refl : ('a, 'a) le
-(** Reflexivity of anteriority *)
-
-val cons : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
-(** Transitivity of anteriority *)
-
-val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
-(** Alias for {!cons} *)
-
-(** {5 Monotonous evarmaps} *)
-
-type 'r t
-(** Stage-indexed evarmaps. This is just a plain evarmap with a phantom type. *)
-
-type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
-(** Return values at a later stage *)
-
-type 'r evar
-(** Stage-indexed evars *)
-
-(** {5 Constructors} *)
-
-val here : 'a -> 'r t -> ('a, 'r) sigma
-(** [here x s] is a shorthand for [Sigma (x, s, refl)] *)
-
-(** {5 Postponing} *)
-
-val lift_evar : 'r evar -> ('r, 's) le -> 's evar
-(** Any evar existing at stage ['r] is also valid at any later stage. *)
-
-(** {5 Downcasting} *)
-
-val to_evar_map : 'r t -> Evd.evar_map
-val to_evar : 'r evar -> Evar.t
-
-(** {5 Monotonous API} *)
-
-type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
-
-val new_evar : 'r t -> ?name:Id.t ->
-  Evd.evar_info -> 'r fresh
-
-val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
-
-(** Polymorphic universes *)
-
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string ->
-  Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
-val new_univ_variable : ?loc:Loc.t -> ?name:string ->
-  Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
-val new_sort_variable : ?loc:Loc.t -> ?name:string ->
-  Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
-
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->
-  'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
-val fresh_constant_instance :
-  ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
-val fresh_inductive_instance :
-  ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
-val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor ->
-  (pconstructor, 'r) sigma
-
-val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
-  'r t -> Globnames.global_reference -> (constr, 'r) sigma
-
-(** FILLME *)
-
-(** {5 Run} *)
-
-type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
-
-val run : Evd.evar_map -> 'a run -> 'a * Evd.evar_map
-
-(** {5 Imperative monotonic functions} *)
-
-type evdref
-(** Monotonic references over evarmaps *)
-
-val apply : evdref -> 'a run -> 'a
-(** Apply a monotonic function on a reference. *)
-
-val purify : (evdref -> 'a) -> 'a run
-(** Converse of {!apply}. *)
-
-(** {5 Unsafe primitives} *)
-
-module Unsafe :
-sig
-  val le : ('a, 'b) le
-  val of_evar_map : Evd.evar_map -> 'r t
-  val of_evar : Evd.evar -> 'r evar
-  val of_ref : Evd.evar_map ref -> evdref
-  val of_pair : ('a * Evd.evar_map) -> ('a, 'r) sigma
-end
-
-(** {5 Notations} *)
-
-module Notations :
-sig
-  type ('a, 'r) sigma_ = ('a, 'r) sigma =
-    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
-
-  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
-
-  val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
-  (** Alias for {!cons} *)
-end