diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-29 12:57:35 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-29 12:57:35 +0000 |
| commit | 5094f4879cf86d7cbc5879d3acd9216ea2615f87 (patch) | |
| tree | 6434518a71398ca4b52315102f4c65abbfc74032 /parsing/pretty.mli | |
| parent | 2a49a1239b1e69fa0eb5695166fe9808c9774314 (diff) | |
portage Astterm (partiellement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pretty.mli')
| -rw-r--r-- | parsing/pretty.mli | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/parsing/pretty.mli b/parsing/pretty.mli index 2b4c378c2..dd8d605ed 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -27,18 +27,23 @@ val print_full_context_typ : unit -> std_ppcmds val print_crible : identifier -> unit val print_sec_context : string -> std_ppcmds val print_sec_context_typ : string -> std_ppcmds -val print_val : context -> unsafe_judgment -> std_ppcmds -val print_type : context -> unsafe_judgment -> std_ppcmds +val print_val : unsafe_env -> unsafe_judgment -> std_ppcmds +val print_type : unsafe_env -> unsafe_judgment -> std_ppcmds val print_eval : - 'a reduction_function -> context -> unsafe_judgment -> std_ppcmds -val implicit_args_msg : mutual_inductive_packet array -> std_ppcmds -val print_mutual : path_kind -> mutual_inductive_body -> std_ppcmds + 'a reduction_function -> unsafe_env -> unsafe_judgment -> std_ppcmds +val implicit_args_msg : + section_path -> mutual_inductive_packet array -> std_ppcmds +val print_mutual : section_path -> mutual_inductive_body -> std_ppcmds val print_name : identifier -> std_ppcmds val print_opaque_name : identifier -> std_ppcmds val print_local_context : unit -> std_ppcmds + +(*i val print_extracted_name : identifier -> std_ppcmds val print_extraction : unit -> std_ppcmds val print_extracted_vars : unit -> std_ppcmds +i*) + val crible : (string -> unit assumptions -> constr -> unit) -> identifier -> unit val inspect : int -> std_ppcmds |