Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 11 insertions, 10 deletions

diff --git a/printing/printer.mli b/printing/printer.mli
index 5f56adbe6f..70993bb727 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,6 @@ open Pp
 open Names
 open Globnames
 open Term
-open Context
 open Environ
 open Pattern
 open Evd
@@ -84,7 +83,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 *)
 
@@ -108,13 +108,13 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
 
-val pr_var_decl            : env -> evar_map -> named_declaration -> std_ppcmds
-val pr_var_list_decl       : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl            : env -> evar_map -> rel_declaration -> std_ppcmds
+val pr_var_decl            : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_var_list_decl       : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
 
-val pr_named_context       : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds
 val pr_named_context_of    : env -> evar_map -> std_ppcmds
-val pr_rel_context         : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context         : env -> evar_map -> Context.Rel.t -> std_ppcmds
 val pr_rel_context_of      : env -> evar_map -> std_ppcmds
 val pr_context_of          : env -> evar_map -> std_ppcmds
 
@@ -164,7 +164,7 @@ val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 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
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
 
@@ -175,7 +175,8 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset :
   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;