[api] Insert miscellaneous API deprecation back to core.

7 files changed, 16 insertions, 14 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 21a65f8eb..d676a0874 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -95,14 +95,14 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
     tactic. *)
 
 val build_constant_by_tactic :
-  Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
+  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
   EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
-    Evd.evar_universe_context
+    UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
   EConstr.types -> unit Proofview.tactic -> 
-  constr * bool * Evd.evar_universe_context
+  constr * bool * UState.t
 
 val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
diff --git a/proofs/proof.ml b/proofs/proof.ml
index ba4980b66..e24d57f08 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -112,7 +112,7 @@ type proof = {
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
   (* The initial universe context (for the statement) *)
-  initial_euctx : Evd.evar_universe_context
+  initial_euctx : UState.t
 }
 
 (*** General proof functions ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 698aa48b0..48aed8225 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -69,7 +69,7 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
 val initial_goals : proof -> (EConstr.constr * EConstr.types) list
-val initial_euctx : proof -> Evd.evar_universe_context
+val initial_euctx : proof -> UState.t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8b788bb38..fdc9a236b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,7 +68,7 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
   let levels = Univ.Instance.levels (Univ.UContext.instance init) in
   UState.constrain_variables levels uctx
 
-type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6309f681f..eed62f912 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -33,7 +33,7 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
@@ -86,7 +86,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9c8777c41..34e517aed 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -35,10 +35,10 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclEVARUNIVCONTEXT : UState.t -> tactic
 
 val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
-val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
 val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 6441cfd19..d9496d2b4 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -10,7 +10,6 @@ open Names
 open Constr
 open Environ
 open EConstr
-open Evd
 open Proof_type
 open Redexpr
 open Pattern
@@ -19,7 +18,10 @@ open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
-type 'a sigma   = 'a Evd.sigma;;
+type 'a sigma   = 'a Evd.sigma
+[@@ocaml.deprecated "alias of Evd.sigma"]
+
+open Evd
 type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a