4 files changed, 13 insertions, 13 deletions
diff --git a/vernac/command.mli b/vernac/command.mli
index 5415d3308..fb99a717b 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -127,24 +127,24 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+  recursive_preentry * Univdecls.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
-  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+  recursive_preentry * Univdecls.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1f46a385d..6972edd52 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -27,10 +27,10 @@ val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_m
    unit declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
-  ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+  ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
-  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
+  (UState.t option -> unit declaration_hook) -> unit
 
 val start_proof_com :
   ?inference_hook:Pretyping.inference_hook ->
@@ -46,7 +46,7 @@ val start_proof_with_initialization :
 
 val universe_proof_terminator :
   Proof_global.lemma_possible_guards ->
-    (Evd.evar_universe_context option -> unit declaration_hook) ->
+    (UState.t option -> unit declaration_hook) ->
     Proof_global.proof_terminator
 
 val standard_proof_terminator :
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 364557bb4..ed4d8b888 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -304,7 +304,7 @@ type program_info_aux = {
   prg_name: Id.t;
   prg_body: constr;
   prg_type: constr;
-  prg_ctx:  Evd.evar_universe_context;
+  prg_ctx:  UState.t;
   prg_univdecl: Univdecls.universe_decl;
   prg_obligations: obligations;
   prg_deps : Id.t list;
@@ -313,7 +313,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
+  prg_hook : (UState.t -> unit) Lemmas.declaration_hook;
   prg_opaque : bool;
   prg_sign: named_context_val;
 }
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index d037fdcd8..481faadb8 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -52,13 +52,13 @@ type progress = (* Resolution status of a program *)
 val default_tactic : unit Proofview.tactic ref
 
 val add_definition : Names.Id.t -> ?term:constr -> types -> 
-  Evd.evar_universe_context ->
+  UState.t ->
   ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(constr -> constr) ->
-  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -70,12 +70,12 @@ type fixpoint_kind =
 val add_mutual_definitions :
   (Names.Id.t * constr * types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
-  Evd.evar_universe_context ->
+  UState.t ->
   ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit