diff options
| author | herbelin | 2000-07-24 13:39:23 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-24 13:39:23 +0000 |
| commit | 3afaf3dde673d77cacaabc354f008dfbe49a7cee (patch) | |
| tree | 4264164faf763ab8d18274cd5aeffe5a1de21728 /parsing/pretty.mli | |
| parent | 83f038e61a4424fcf71aada9f97c91165b73aef8 (diff) | |
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
Diffstat (limited to 'parsing/pretty.mli')
| -rw-r--r-- | parsing/pretty.mli | 5 |
1 files changed, 2 insertions, 3 deletions
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 |