[api] Insert miscellaneous API deprecation back to core.

22 files changed, 68 insertions, 59 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 45ca1a365..af5373582 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -125,6 +125,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info
 (** {6 Unification state} **)
 
 type evar_universe_context = UState.t
+[@@ocaml.deprecated "Alias of UState.t"]
 (** The universe context associated to an evar map *)
 
 type evar_map
@@ -138,7 +139,7 @@ val from_env : env -> evar_map
 (** The empty evar map with given universe context, taking its initial 
     universes from env. *)
 
-val from_ctx : evar_universe_context -> evar_map
+val from_ctx : UState.t -> evar_map
 (** The empty evar map with given universe context *)
 
 val is_empty : evar_map -> bool
@@ -486,37 +487,37 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-type 'a in_evar_universe_context = 'a * evar_universe_context
+type 'a in_evar_universe_context = 'a * UState.t
 
-val evar_universe_context_set : evar_universe_context -> Univ.ContextSet.t
-val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
-val evar_context_universe_context : evar_universe_context -> Univ.UContext.t
-val evar_universe_context_of : Univ.ContextSet.t -> evar_universe_context
-val empty_evar_universe_context : evar_universe_context
-val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
-  evar_universe_context
-val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
-val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context
+val evar_universe_context_set : UState.t -> Univ.ContextSet.t
+val evar_universe_context_constraints : UState.t -> Univ.constraints
+val evar_context_universe_context : UState.t -> Univ.UContext.t
+val evar_universe_context_of : Univ.ContextSet.t -> UState.t
+val empty_evar_universe_context : UState.t
+val union_evar_universe_context : UState.t -> UState.t ->
+  UState.t
+val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst
+val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 
 
 val evar_universe_context_of_binders :
-  Universes.universe_binders -> evar_universe_context
+  Universes.universe_binders -> UState.t
 							    
-val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
+val make_evar_universe_context : env -> (Id.t located) list option -> UState.t
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map							   
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> string -> Univ.Level.t
 val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map
 
-val add_constraints_context : evar_universe_context -> 
-  Univ.constraints -> evar_universe_context
+val add_constraints_context : UState.t -> 
+  Univ.constraints -> UState.t
 
 
-val normalize_evar_universe_context_variables : evar_universe_context -> 
+val normalize_evar_universe_context_variables : UState.t -> 
   Univ.universe_subst in_evar_universe_context
 
-val normalize_evar_universe_context : evar_universe_context -> 
-  evar_universe_context
+val normalize_evar_universe_context : UState.t -> 
+  UState.t
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t
 val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -548,7 +549,7 @@ val set_eq_instances : ?flex:bool ->
 val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 
-val evar_universe_context : evar_map -> evar_universe_context
+val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
 val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
 		       (Id.t * Univ.Level.t) list * Univ.UContext.t
@@ -558,8 +559,8 @@ val universes : evar_map -> UGraph.t
 val check_univ_decl : evar_map -> UState.universe_decl ->
   Universes.universe_binders * Univ.UContext.t
 
-val merge_universe_context : evar_map -> evar_universe_context -> evar_map
-val set_universe_context : evar_map -> evar_universe_context -> evar_map
+val merge_universe_context : evar_map -> UState.t -> evar_map
+val set_universe_context : evar_map -> UState.t -> evar_map
 
 val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
 val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
@@ -567,7 +568,7 @@ val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
 val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
-val abstract_undefined_variables : evar_universe_context -> evar_universe_context
+val abstract_undefined_variables : UState.t -> UState.t
 
 val fix_undefined_variables : evar_map -> evar_map
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index d92d0a7d5..0379d4b49 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -426,7 +426,7 @@ module Unsafe : sig
   val tclGETGOALS : Evd.evar list tactic
 
   (** Sets the evar universe context. *)
-  val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
+  val tclEVARUNIVCONTEXT : UState.t -> unit tactic
 
   (** Clears the future goals store in the proof view. *)
   val reset_future_goals : proofview -> proofview
diff --git a/engine/termops.mli b/engine/termops.mli
index 2dab0685d..793490798 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -113,6 +113,7 @@ val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
 val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
 val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
+[@@ocaml.deprecated "alias of Termops.dependent"]
 
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
@@ -290,7 +291,7 @@ val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t
 val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
   evar_map -> Pp.t
 val pr_metaset : Metaset.t -> Pp.t
-val pr_evar_universe_context : evar_universe_context -> Pp.t
+val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
 (** debug printer: do not use to display terms to the casual user... *)
diff --git a/library/globnames.mli b/library/globnames.mli
index 5c484b391..2e0cd62db 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -47,6 +47,7 @@ val global_of_constr : constr -> global_reference
 
 (** Obsolete synonyms for constr_of_global and global_of_constr *)
 val reference_of_constr : constr -> global_reference
+[@@ocaml.deprecated "Alias of Globnames.global_of_constr"]
 
 module RefOrdered : sig
   type t = global_reference
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index be96cfce5..1320cce9b 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -43,6 +43,8 @@ val pr_sep_com :
 
 val pr_id : Id.t -> Pp.t
 val pr_name : Name.t -> Pp.t
+[@@ocaml.deprecated "alias of Names.Name.print"]
+
 val pr_qualid : qualid -> Pp.t
 val pr_patvar : patvar -> Pp.t
 
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
diff --git a/stm/stm.ml b/stm/stm.ml
index 6c22d3771..b394c3a13 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1749,7 +1749,7 @@ end (* }}} *)
 
 and TacTask : sig
 
-  type output = (Constr.constr * Evd.evar_universe_context) option
+  type output = (Constr.constr * UState.t) option
   type task = {
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
@@ -1763,7 +1763,7 @@ and TacTask : sig
 
 end = struct (* {{{ *)
 
-  type output = (Constr.constr * Evd.evar_universe_context) option
+  type output = (Constr.constr * UState.t) option
   
   let forward_feedback msg = Hooks.(call forward_feedback msg)
 
@@ -1785,7 +1785,7 @@ end = struct (* {{{ *)
     r_name     : string }
 
   type response =
-    | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context)
+    | RespBuiltSubProof of (Constr.constr * UState.t)
     | RespError of Pp.t
     | RespNoProgress
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7eae2541e..239661498 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -16,6 +16,7 @@ open EConstr
 open Proof_type
 open Tacticals
 open Tacmach
+open Evd
 open Tactics
 open Clenv
 open Auto
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 9c750e7ad..50b052f23 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -16,7 +16,7 @@ val optimize_non_type_induction_scheme :
   Sorts.family ->
   'b ->
   Names.inductive ->
-  (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants
+  (Constr.constr * UState.t) * Safe_typing.private_constants
 
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7b2445ff5..c36ad980e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1824,9 +1824,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
       match EConstr.kind sigma x, EConstr.kind sigma y with
-      | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
+      | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f5c209c74..169ac5c90 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,7 +9,7 @@
 open Names
 open Constr
 open EConstr
-open Tacmach
+open Evd
 open Proof_type
 open Locus
 open Misctypes
@@ -23,6 +23,7 @@ val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
 val tclTHENSEQ       : tactic list -> tactic
+[@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"]
 val tclTHENLIST      : tactic list -> tactic
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 val tclTHENFIRST     : tactic -> tactic -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 096274c68..15c25b346 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1476,7 +1476,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let sort = Tacticals.New.elimination_sort_of_goal gl in
   let mind = on_snd (fun u -> EInstance.kind sigma u) mind in
   let (sigma, elim) =
-    if occur_term sigma c concl then
+    if dependent sigma c concl then
       build_case_analysis_scheme env sigma mind true sort
     else
       build_case_analysis_scheme_default env sigma mind sort in
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