Merge PR#623: Remove the Sigma (monotonous state) API.

9 files changed, 58 insertions, 73 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d6ed201d84..79d2e46942 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 4bcd50591c..f43c0531d4 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 0722ea0470..2ce144a6d7 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 5a717f1662..e69ef18fd0 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 383a6a5233..458dd21613 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 63ae41075c..caa6b9fb30 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 5098f246a0..f1439f9a13 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 66d91c634a..f9d9f25ccf 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 1172e55ac6..3d2fa72c17 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