1 files changed, 10 insertions, 8 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index bf35fd65..854ceaa4 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit
 val get_current_proof_name : unit -> Names.Id.t
 val get_all_proof_names : unit -> Names.Id.t list
 
-val discard : Misctypes.lident -> unit
+val discard : Names.lident -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
@@ -48,11 +48,13 @@ type proof_object = {
   universes: UState.t;
 }
 
+type opacity_flag = Opaque | Transparent
+
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
                 UState.t
-  | Proved of Vernacexpr.opacity_flag *
-              Misctypes.lident option *
+  | Proved of opacity_flag *
+              Names.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
@@ -69,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
+  Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -124,11 +126,11 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * Misctypes.lident list
-val get_used_variables : unit -> Context.Named.t option
+  Names.Id.t list -> Constr.named_context * Names.lident list
+val get_used_variables : unit -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> Univdecls.universe_decl
+val get_universe_decl : unit -> UState.universe_decl
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *