diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:58:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:58:53 +0000 |
| commit | 30d5964b04b8d724b838c3ceb1244267d5d4c70a (patch) | |
| tree | de77df17da8002d3fee9862c4b91a75c633f7ab2 /parsing/pretty.mli | |
| parent | e304d37c1c90b88954cbd224070c9a2326ab06f2 (diff) | |
Prise en compte des noms qualifiés dans certaines commandes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@884 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pretty.mli')
| -rw-r--r-- | parsing/pretty.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pretty.mli b/parsing/pretty.mli index 811e663de..946965c6d 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -22,7 +22,6 @@ 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 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 : env -> unsafe_judgment -> std_ppcmds @@ -48,7 +47,8 @@ val print_coercions : unit -> std_ppcmds val print_path_between : identifier -> identifier -> std_ppcmds -val crible : (string -> env -> constr -> unit) -> identifier -> +val search_by_head : global_reference -> unit +val crible : (string -> env -> constr -> unit) -> global_reference -> unit val inspect : int -> std_ppcmds |