From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 29 Apr 2010 09:56:37 +0000 Subject: Move from ocamlweb to ocamdoc to generate mli documentation dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.mli | 36 +++++++++++++++++------------------- 1 file changed, 17 insertions(+), 19 deletions(-) (limited to 'interp/constrextern.mli') diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 08a74e614..f52ec8fd8 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* v8 translation *) +(** v7->v8 translation *) val check_same_type : constr_expr -> constr_expr -> unit -(* Translation of pattern, cases pattern, rawterm and term into syntax +(** Translation of pattern, cases pattern, rawterm and term into syntax trees for printing *) val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr @@ -34,7 +32,7 @@ val extern_rawconstr : Idset.t -> rawconstr -> constr_expr val extern_rawtype : Idset.t -> rawconstr -> constr_expr val extern_constr_pattern : names_context -> constr_pattern -> constr_expr -(* If [b=true] in [extern_constr b env c] then the variables in the first +(** If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed *) val extern_constr : bool -> env -> constr -> constr_expr @@ -45,7 +43,7 @@ val extern_sort : sorts -> rawsort val extern_rel_context : constr option -> env -> rel_context -> local_binder list -(* Printing options *) +(** Printing options *) val print_implicits : bool ref val print_implicits_defensive : bool ref val print_arguments : bool ref @@ -55,25 +53,25 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -(* Debug printing options *) +(** Debug printing options *) val set_debug_global_reference_printer : (loc -> global_reference -> reference) -> unit -(* This governs printing of implicit arguments. If [with_implicits] is +(** This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed by "!"; if [with_implicits] and [with_arguments] are both on the function and not the arguments is prefixed by "!" *) val with_implicits : ('a -> 'b) -> 'a -> 'b val with_arguments : ('a -> 'b) -> 'a -> 'b -(* This forces printing of coercions *) +(** This forces printing of coercions *) val with_coercions : ('a -> 'b) -> 'a -> 'b -(* This forces printing universe names of Type{.} *) +(** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b -(* This suppresses printing of numeral and symbols *) +(** This suppresses printing of numeral and symbols *) val without_symbols : ('a -> 'b) -> 'a -> 'b -(* This prints metas as anonymous holes *) +(** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3