From 3afaf3dde673d77cacaabc354f008dfbe49a7cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:39:23 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'parsing/pretty.mli')

diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index e10c53b802..dd7378d416 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -13,13 +13,12 @@ open Environ
 
 (* A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
-val assumptions_for_print : name list -> unit assumptions
+val assumptions_for_print : name list -> names_context
 
 val print_basename : section_path -> string
 val print_basename_mind : section_path -> identifier -> string
 val print_closed_sections : bool ref
 val print_impl_args : int list -> std_ppcmds
-val print_env : path_kind -> (name * constr) list -> std_ppcmds
 val print_context : bool -> Lib.library_segment -> std_ppcmds
 val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds
 val print_full_context : unit -> std_ppcmds
@@ -50,7 +49,7 @@ val print_coercions : unit -> std_ppcmds
 val print_path_between : identifier -> identifier -> std_ppcmds
 
 
-val crible : (string -> unit assumptions -> constr -> unit) -> identifier ->
+val crible : (string -> env -> constr -> unit) -> identifier ->
   unit
 val inspect : int -> std_ppcmds
 
-- 
cgit v1.2.3