diff options
author | 2001-05-28 12:14:49 +0000 | |
---|---|---|
committer | 2001-05-28 12:14:49 +0000 | |
commit | 6dc94fe5c1e02fccefbfedfcb1d4347274f3de0b (patch) | |
tree | 4a33333de304fb331f0f7b2b9ea761a8301b2f8d /parsing/pretty.mli | |
parent | 47bde1826b6329650f8546ac1fca1f2e90d85fcb (diff) |
Pretty -> Prettyp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pretty.mli')
-rw-r--r-- | parsing/pretty.mli | 59 |
1 files changed, 0 insertions, 59 deletions
diff --git a/parsing/pretty.mli b/parsing/pretty.mli deleted file mode 100644 index b84c56634..000000000 --- a/parsing/pretty.mli +++ /dev/null @@ -1,59 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -(*i*) -open Pp -open Names -open Sign -open Term -open Inductive -open Reduction -open Environ -(*i*) - -(* A Pretty-Printer for the Calculus of Inductive Constructions. *) - -val assumptions_for_print : name list -> names_context - -val print_closed_sections : bool ref -val print_impl_args : int 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 -val print_full_context_typ : unit -> std_ppcmds -val print_sec_context : Nametab.qualid -> std_ppcmds -val print_sec_context_typ : Nametab.qualid -> std_ppcmds -val print_judgment : env -> unsafe_judgment -> std_ppcmds -val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds -val print_eval : - 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds -(* This function is exported for the graphical user-interface pcoq *) -val build_inductive : section_path -> int -> - global_reference * rel_context * types * identifier array * types array -val print_mutual : section_path -> std_ppcmds -val print_name : Nametab.qualid -> std_ppcmds -val print_opaque_name : Nametab.qualid -> 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*) - -(* 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 : identifier -> identifier -> std_ppcmds - - -val inspect : int -> std_ppcmds - |