Imported Upstream version 8.5~beta3+dfsg

1 files changed, 17 insertions, 5 deletions

diff --git a/printing/printer.mli b/printing/printer.mli
index a469a8db..5c60b893 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -84,7 +84,8 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
-val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
+val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
@@ -160,12 +161,23 @@ val emacs_str              : string -> string
 val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 
 
-(** spiwack: printer function for sets of Environ.assumption.
-            It is used primarily by the Print Assumption command. *)
+(** Declarations for the "Print Assumption" command *)
+type context_object =
+  | Variable of Id.t  (** A section variable or a Let definition *)
+  (** An axiom and the type it inhabits (if an axiom of the empty type) *)
+  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Opaque of constant      (** An opaque constant. *)
+  | Transparent of constant (** A transparent constant *)
+
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : CMap.ExtS
+  with type key = context_object and module Set := ContextObjectSet
+
 val pr_assumptionset :
-  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
+  env -> Term.types ContextObjectMap.t -> std_ppcmds
 
-val pr_goal_by_id : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> std_ppcmds
+val pr_goal_by_uid : string -> std_ppcmds
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;