From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 parsing/prettyp.mli | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

(limited to 'parsing/prettyp.mli')

diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index fef66a63..6d9c6ecc 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: prettyp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Pp
 open Util
 open Names
@@ -19,9 +16,8 @@ open Reductionops
 open Libnames
 open Nametab
 open Genarg
-(*i*)
 
-(* A Pretty-Printer for the Calculus of Inductive Constructions. *)
+(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
 val assumptions_for_print : name list -> Termops.names_context
 
@@ -37,29 +33,27 @@ val print_judgment : env -> unsafe_judgment -> std_ppcmds
 val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
   reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
-(* This function is exported for the graphical user-interface pcoq *)
-val build_inductive : mutual_inductive -> int ->
-  global_reference * rel_context * types * identifier array * types array
+
 val print_name : reference or_by_notation -> std_ppcmds
 val print_opaque_name : reference -> std_ppcmds
 val print_about : reference or_by_notation -> std_ppcmds
 val print_impargs : reference or_by_notation -> std_ppcmds
 
-(* Pretty-printing functions for classes and coercions *)
+(** Pretty-printing functions for classes and coercions *)
 val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
 val print_canonical_projections : unit -> std_ppcmds
 
-(* Pretty-printing functions for type classes and instances *)
+(** Pretty-printing functions for type classes and instances *)
 val print_typeclasses : unit -> std_ppcmds
 val print_instances : global_reference -> std_ppcmds
 val print_all_instances : unit -> std_ppcmds
 
 val inspect : int -> std_ppcmds
 
-(* Locate *)
+(** Locate *)
 val print_located_qualid : reference -> std_ppcmds
 
 type object_pr = {
@@ -70,7 +64,6 @@ type object_pr = {
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
   print_named_decl          : identifier * constr option * types -> std_ppcmds;
-  print_leaf_entry          : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
-- 
cgit v1.2.3