From ccba6c718af6a5a15f278fc9365b6ad27108e98f Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 29 Apr 2010 16:06:42 +0000 Subject: Various minor improvements of comments in mli for ocamldoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrintern.mli | 8 ++--- interp/coqlib.mli | 7 ++-- interp/notation.mli | 15 +++----- interp/topconstr.mli | 27 ++++++--------- kernel/cemitcodes.mli | 2 +- kernel/closure.mli | 2 +- kernel/environ.mli | 2 +- kernel/esubst.mli | 40 +++++++++++----------- kernel/indtypes.mli | 4 +-- kernel/inductive.mli | 2 +- kernel/mod_subst.mli | 3 +- kernel/names.mli | 2 +- kernel/safe_typing.mli | 6 ++-- kernel/sign.mli | 2 +- kernel/term.mli | 8 ++--- kernel/univ.mli | 2 +- kernel/vm.mli | 25 ++++++++++---- lib/explore.mli | 4 +-- lib/pp.mli | 2 +- lib/system.mli | 12 ++++--- lib/util.mli | 4 +-- library/declaremods.mli | 6 ++-- library/dischargedhypsmap.mli | 1 - library/global.mli | 5 ++- library/impargs.mli | 8 +++-- library/lib.mli | 9 ++--- library/libnames.mli | 4 +-- library/libobject.mli | 2 +- library/library.mli | 7 ++-- library/nametab.mli | 79 ++++++++++++++++++++----------------------- library/states.mli | 12 +++---- pretyping/classops.mli | 3 +- pretyping/evarconv.mli | 3 +- pretyping/evd.mli | 2 +- pretyping/pretyping.mli | 3 +- pretyping/recordops.mli | 6 ++-- pretyping/termops.mli | 2 +- proofs/pfedit.mli | 20 +++++------ proofs/proof_type.mli | 2 +- tactics/auto.mli | 12 ++++--- tactics/hipattern.mli | 4 +-- tactics/termdn.mli | 2 +- toplevel/command.mli | 15 +++----- toplevel/lemmas.mli | 2 +- 44 files changed, 194 insertions(+), 194 deletions(-) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index bf28e0850..880f8a4be 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,19 +18,17 @@ open Topconstr open Termops open Pretyping -(** {6 Sect } *) -(** Translation from front abstract syntax of term to untyped terms (rawconstr) +(** Translation from front abstract syntax of term to untyped terms (rawconstr) *) - The translation performs: +(** The translation performs: - resolution of names : - check all variables are bound - make absolute the references to global objets - resolution of symbolic notations using scopes - insert existential variables for implicit arguments -*) -(** To interpret implicits and arg scopes of recursive variables while + To interpret implicits and arg scopes of recursive variables while internalizing inductive types and recursive definitions, and also projection while typing records. diff --git a/interp/coqlib.mli b/interp/coqlib.mli index a80e749d3..1d7f571b3 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -12,11 +12,10 @@ open Nametab open Term open Pattern -(** {6 Sect } *) (** This module collects the global references, constructions and patterns of the standard library used in ocaml files *) -(** {6 Sect } *) +(** {6 ... } *) (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that @@ -80,7 +79,7 @@ val glob_eq : global_reference val glob_identity : global_reference val glob_jmeq : global_reference -(** {6 Sect } *) +(** {6 ... } *) (** Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and @@ -144,7 +143,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed (** Specif *) val build_coq_sumbool : constr delayed -(** {6 Sect } *) +(** {6 ... } *) (** Connectives The False proposition *) val build_coq_False : constr delayed diff --git a/interp/notation.mli b/interp/notation.mli index 224fb1d45..3da9ec0e5 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -16,12 +16,9 @@ open Rawterm open Topconstr open Ppextend -(**/**) +(** Notations *) -(********************************************************************* - Scopes *) - -(** {6 Sect } *) +(** {6 Scopes } *) (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) @@ -131,7 +128,7 @@ val availability_of_notation : scope_name option * notation -> local_scopes -> val declare_notation_level : notation -> level -> unit val level_of_notation : notation -> level (** raise [Not_found] if no level *) -(*s** Miscellaneous *) +(** {6 Miscellaneous} *) val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> notation -> delimiters option -> global_reference @@ -170,13 +167,11 @@ val locate_notation : (rawconstr -> std_ppcmds) -> notation -> val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds -(********************************************************************* - s Printing rules for notations *) +(** {6 Printing rules for notations} *) (** Declare and look for the printing rule for symbolic notations *) type unparsing_rule = unparsing list * precedence val declare_notation_printing_rule : notation -> unparsing_rule -> unit val find_notation_printing_rule : notation -> unparsing_rule -(********************************************************************* - Rem: printing rules for primitive token are canonical *) +(** Rem: printing rules for primitive token are canonical *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 2b9506747..8f1fa5c3d 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -14,7 +14,9 @@ open Rawterm open Term open Mod_subst -(** {6 Sect } *) +(** Topconstr: definitions of [aconstr] et [constr_expr] *) + +(** {6 aconstr } *) (** This is the subtype of rawconstr allowed in syntactic extensions No location since intended to be substituted at any place of a text Complex expressions such as fixpoints and cofixpoints are excluded, @@ -43,9 +45,8 @@ type aconstr = | APatVar of patvar | ACast of aconstr * aconstr cast_type -(********************************************************************* - Translate a rawconstr into a notation given the list of variables - bound by the notation; also interpret recursive patterns *) +(** Translate a rawconstr into a notation given the list of variables + bound by the notation; also interpret recursive patterns *) val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr @@ -55,8 +56,7 @@ val ldots_var : identifier (** Equality of rawconstr (warning: only partially implemented) *) val eq_rawconstr : rawconstr -> rawconstr -> bool -(********************************************************************* - Re-interpret a notation as a rawconstr, taking care of binders *) +(** Re-interpret a notation as a rawconstr, taking care of binders *) val rawconstr_of_aconstr_with_binders : loc -> ('a -> name -> 'a * name) -> @@ -64,8 +64,7 @@ val rawconstr_of_aconstr_with_binders : loc -> val rawconstr_of_aconstr : loc -> aconstr -> rawconstr -(********************************************************************* - [match_aconstr metas] matches a rawconstr against an aconstr with +(** [match_aconstr metas] matches a rawconstr against an aconstr with metavariables in [metas]; raise [No_match] if the matching fails *) exception No_match @@ -83,13 +82,11 @@ type interpretation = val match_aconstr : rawconstr -> interpretation -> (rawconstr * subscopes) list * (rawconstr list * subscopes) list -(********************************************************************* - Substitution of kernel names in interpretation data *) +(** Substitution of kernel names in interpretation data *) val subst_interpretation : substitution -> interpretation -> interpretation -(********************************************************************* - s Concrete syntax for terms *) +(** {6 Concrete syntax for terms } *) type notation = string @@ -172,8 +169,7 @@ and typeclass_context = typeclass_constraint list type constr_pattern_expr = constr_expr -(********************************************************************* - Utilities on constr_expr *) +(** Utilities on constr_expr *) val constr_loc : constr_expr -> loc @@ -231,8 +227,7 @@ val map_constr_expr_with_binders : (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> 'a -> constr_expr -> constr_expr -(********************************************************************* - Concrete syntax for modules and module types *) +(** Concrete syntax for modules and module types *) type with_declaration_ast = | CWith_Module of identifier list located * qualid located diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 547155423..a8ecc82b4 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -8,7 +8,7 @@ type reloc_info = type patch = reloc_info * int -(** A virer *) +(* A virer *) val subst_patch : Mod_subst.substitution -> patch -> patch type emitcodes diff --git a/kernel/closure.mli b/kernel/closure.mli index d482e91b2..9a8ced44e 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -18,7 +18,7 @@ val share : bool ref val with_stats: 'a Lazy.t -> 'a -(** {6 Sect } *) +(** {6 ... } *) (** Delta implies all consts (both global (= by [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of diff --git a/kernel/environ.mli b/kernel/environ.mli index 0ecfa21b6..8c31742f3 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -120,7 +120,7 @@ val add_constant : constant -> constant_body -> env -> env val lookup_constant : constant -> env -> constant_body val evaluable_constant : constant -> env -> bool -(** {6 Sect } *) +(** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no body and [Not_found] if it does not exist in [env] *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index fd7753093..dd7096c4b 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -6,13 +6,15 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {6 Sect } *) +(** Explicit substitutions *) + +(** {6 Explicit substitutions } *) (** Explicit substitutions of type ['a]. - ESID(n) = %n END bounded identity - * - CONS([|t1..tn|],S) = (S.t1...tn) parallel substitution - * (beware of the order: indice 1 is substituted by tn) - * - SHIFT(n,S) = (^n o S) terms in S are relocated with n vars - * - LIFT(n,S) = (%n S) stands for ((^n o S).n...1) + - CONS([|t1..tn|],S) = (S.t1...tn) parallel substitution + (beware of the order: indice 1 is substituted by tn) + - SHIFT(n,S) = (^n o S) terms in S are relocated with n vars + - LIFT(n,S) = (%n S) stands for ((^n o S).n...1) (corresponds to S crossing n binders) *) type 'a subs = | ESID of int @@ -30,28 +32,28 @@ val subs_liftn: int -> 'a subs -> 'a subs val subs_shift_cons: int * 'a subs * 'a array -> 'a subs (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution - * [subs]. The result is either (Inl(lams,v)) when the variable is - * substituted by value [v] under lams binders (i.e. v *has* to be - * shifted by lams), or (Inr (k',p)) when the variable k is just relocated - * as k'; p is None if the variable points inside subs and Some(k) if the - * variable points k bindings beyond subs (cf argument of ESID). - *) + [subs]. The result is either (Inl(lams,v)) when the variable is + substituted by value [v] under lams binders (i.e. v *has* to be + shifted by lams), or (Inr (k',p)) when the variable k is just relocated + as k'; p is None if the variable points inside subs and Some(k) if the + variable points k bindings beyond subs (cf argument of ESID). +*) val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union (** Tests whether a substitution behaves like the identity *) val is_subs_id: 'a subs -> bool (** Composition of substitutions: [comp mk_clos s1 s2] computes a - * substitution equivalent to applying s2 then s1. Argument - * mk_clos is used when a closure has to be created, i.e. when - * s1 is applied on an element of s2. - *) + substitution equivalent to applying s2 then s1. Argument + mk_clos is used when a closure has to be created, i.e. when + s1 is applied on an element of s2. +*) val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs -(** {6 Sect } *) -(** Compact representation of explicit relocations. \\ - [ELSHFT(l,n)] == lift of [n], then apply [lift l]. - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) +(** {6 Compact representation } *) +(** Compact representation of explicit relocations + - [ELSHFT(l,n)] == lift of [n], then apply [lift l]. + - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) type lift = | ELID | ELSHFT of lift * int diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 388eb21e4..a3867c6b8 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,8 +14,8 @@ open Environ open Entries open Typeops +(** Inductive type checking and errors *) -(** {6 Sect } *) (** The different kinds of errors that may result of a malformed inductive definition. *) @@ -34,7 +34,7 @@ type inductive_error = exception InductiveError of inductive_error -(** {6 The following function does checks on inductive declarations. } *) +(** The following function does checks on inductive declarations. *) val check_inductive : env -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 259e1decd..3212b8eed 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -26,7 +26,7 @@ val find_coinductive : env -> types -> inductive * constr list type mind_specif = mutual_inductive_body * one_inductive_body -(** {6 Sect } *) +(** {6 ... } *) (** Fetching information in the environment about an inductive type. Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index e22a3eb7d..2514e409c 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -90,7 +90,8 @@ val from_val : 'a -> 'a substituted val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a val subst_substituted : substitution -> 'a substituted -> 'a substituted -(*i debugging *) +(**/**) +(* debugging *) val debug_string_of_subst : substitution -> string val debug_pr_subst : substitution -> Pp.std_ppcmds val debug_string_of_delta : delta_resolver -> string diff --git a/kernel/names.mli b/kernel/names.mli index ffbc02714..1c74fdee6 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -39,7 +39,7 @@ val empty_dirpath : dir_path val string_of_dirpath : dir_path -> string -(** {6 Sect } *) +(** {6 ... } *) (** Unique identifier to be used as "self" in structures and signatures - invisible for users *) type label diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index ce62eeafc..3e1051088 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -12,8 +12,9 @@ open Declarations open Entries open Mod_subst -(** {6 Sect } *) -(** Safe environments. Since we are now able to type terms, we can +(** {6 Safe environments } *) + +(** Since we are now able to type terms, we can define an abstract type of safe environments, where objects are typed before being added. @@ -69,6 +70,7 @@ val set_engagement : engagement -> safe_environment -> safe_environment (** {6 Interactive module functions } *) + val start_module : label -> safe_environment -> module_path * safe_environment diff --git a/kernel/sign.mli b/kernel/sign.mli index 07f3df19e..ddb88287e 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -34,7 +34,7 @@ val fold_named_context_reverse : (** {6 Section-related auxiliary functions } *) val instance_from_named_context : named_context -> constr array -(** {6 Sect } *) +(** {6 ... } *) (** Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) diff --git a/kernel/term.mli b/kernel/term.mli index 3940d74c5..f7819d6e6 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -64,7 +64,7 @@ val eq_constr : constr -> constr -> bool type types = constr -(** {6 Sect } *) +(** {6 ... } *) (** Functions for dealing with constr terms. The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with @@ -253,7 +253,7 @@ val is_Type : constr -> bool val iskind : constr -> bool val is_small : sorts -> bool -(** {6 Sect } *) +(** {6 ... } *) (** Term destructors. Destructor operations are partial functions and raise [invalid_arg "dest*"] if the term has not the expected form. *) @@ -319,7 +319,7 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(** {6 Sect } *) +(** {6 ... } *) (** A {e declaration} has the form (name,body,type). It is either an {e assumption} if [body=None] or a {e definition} if [body=Some actualbody]. It is referred by {e name} if [na] is an @@ -483,7 +483,7 @@ val under_casts : (constr -> constr) -> constr -> constr (** Apply a function under components of Cast if any *) val under_outer_cast : (constr -> constr) -> constr -> constr -(** {6 Sect } *) +(** {6 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types and of a sort *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 3a2ec557f..1634009b3 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -51,7 +51,7 @@ type constraint_function = universe -> universe -> constraints -> constraints val enforce_geq : constraint_function val enforce_eq : constraint_function -(** {6 Sect } *) +(** {6 ... } *) (** Merge of constraints in a universes graph. The function [merge_constraints] merges a set of constraints in a given universes graph. It raises the exception [UniverseInconsistency] if the diff --git a/kernel/vm.mli b/kernel/vm.mli index ff76e7cd5..cd5999f04 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -3,16 +3,18 @@ open Term open Cbytecodes open Cemitcodes +(** Efficient Virtual Machine *) val set_drawinstr : unit -> unit val transp_values : unit -> bool val set_transp_values : bool -> unit -(** le code machine *) +(** Machine code *) + type tcode -(** Les valeurs ***********) +(** Values *) type vprod type vfun @@ -27,11 +29,11 @@ type atom = | Aiddef of id_key * values | Aind of inductive -(** Les zippers *) +(** Zippers *) type zipper = | Zapp of arguments - | Zfix of vfix*arguments (** Peut-etre vide *) + | Zfix of vfix * arguments (** might be empty *) | Zswitch of vswitch type stack = zipper list @@ -49,6 +51,7 @@ type whd = | Vatom_stk of atom * stack (** Constructors *) + val val_of_str_const : structured_constant -> values val val_of_rel : int -> values @@ -63,21 +66,26 @@ val val_of_constant_def : int -> constant -> values -> values external val_of_annot_switch : annot_switch -> values = "%identity" (** Destructors *) + val whd_val : values -> whd (** Arguments *) + val nargs : arguments -> int val arg : arguments -> int -> values (** Product *) + val dom : vprod -> values val codom : vprod -> vfun (** Function *) + val body_of_vfun : int -> vfun -> values val decompose_vfun2 : int -> vfun -> vfun -> int * values * values (** Fix *) + val current_fix : vfix -> int val check_fix : vfix -> vfix -> bool val rec_args : vfix -> int array @@ -85,22 +93,27 @@ val reduce_fix : int -> vfix -> vfun array * values array (** bodies , types *) (** CoFix *) + val current_cofix : vcofix -> int val check_cofix : vcofix -> vcofix -> bool val reduce_cofix : int -> vcofix -> values array * values array - (** bodies , types - Block *) + (** bodies , types *) + +(** Block *) + val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values (** Switch *) + val check_switch : vswitch -> vswitch -> bool val case_info : vswitch -> case_info val type_of_switch : vswitch -> values val branch_of_switch : int -> vswitch -> (int * values) array (** Evaluation *) + val whd_stack : values -> stack -> whd val force_whd : values -> stack -> whd diff --git a/lib/explore.mli b/lib/explore.mli index 0e8eb32be..1f17f8a4c 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -8,7 +8,7 @@ (** {6 Search strategies. } *) -(** {6 Sect } *) +(** {6 ... } *) (** A search problem implements the following signature [SearchProblem]. [state] is the type of states of the search tree. [branching] is the branching function; if [branching s] returns an @@ -31,7 +31,7 @@ module type SearchProblem = sig end -(** {6 Sect } *) +(** {6 ... } *) (** Functor [Make] returns some search functions given a search problem. Search functions raise [Not_found] if no success is found. States are always visited in the order they appear in the diff --git a/lib/pp.mli b/lib/pp.mli index 56e66225c..ca62f82d6 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -89,7 +89,7 @@ val msg_with : Format.formatter -> std_ppcmds -> unit val msgnl_with : Format.formatter -> std_ppcmds -> unit -(** {6 Sect } *) +(** {6 ... } *) (** The following functions are instances of the previous ones on [std_ft] and [err_ft]. *) diff --git a/lib/system.mli b/lib/system.mli index 09142f365..d8a4088d0 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,12 +6,14 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {6 Sect } *) -(** Files and load paths. Load path entries remember the original root +(** System utilities *) + +(** {6 Files and load paths} *) + +(** Load path entries remember the original root given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) - type physical_path = string type load_path = physical_path list @@ -38,7 +40,7 @@ val exists_dir : string -> bool val find_file_in_path : ?warn:bool -> load_path -> string -> physical_path * string -(** {6 Sect } *) +(** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] when the check fails, with the full file name. *) @@ -58,7 +60,7 @@ val extern_intern : ?warn:bool -> int -> string -> val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a -(** {6 Sect } *) +(** {6 Executing commands } *) (** [run_command converter f com] launches command [com], and returns the contents of stdout and stderr that have been processed with [converter]; the processed contents of stdout and stderr is also diff --git a/lib/util.mli b/lib/util.mli index fd8ff9275..f7f40b805 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -11,7 +11,7 @@ open Pp (** This module contains numerous utility functions on strings, lists, arrays, etc. *) -(** {6 Sect } *) +(** {6 ... } *) (** Errors. [Anomaly] is used for system errors and [UserError] for the user's ones. *) @@ -361,7 +361,7 @@ val size_kb : 'a -> int val heap_size : unit -> int val heap_size_kb : unit -> int -(** {6 Sect } *) +(** {6 ... } *) (** Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises [Break], simulating a Ctrl-C) *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 4cbdf4ce4..b7126147e 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -13,9 +13,7 @@ open Environ open Libnames open Libobject open Lib - (**/**) -(** {6 Sect } *) (** This modules provides official functions to declare modules and module types *) @@ -65,7 +63,7 @@ val start_modtype : (env -> 'modast -> module_struct_entry) -> val end_modtype : unit -> module_path -(** {6 Sect } *) +(** {6 ... } *) (** Objects of a module. They come in two lists: the substitutive ones and the other *) @@ -107,7 +105,7 @@ val import_module : bool -> module_path -> unit val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> ('struct_expr * bool) list -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented in an arbitrary order. The given function is applied to all leaves diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index b264c1228..98e3d93d5 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -13,7 +13,6 @@ open Nametab type discharged_hyps = full_path list -(** {6 Sect } *) (** Discharged hypothesis. Here we store the discharged hypothesis of each constant or inductive type declaration. *) diff --git a/library/global.mli b/library/global.mli index ae2ed16f7..d29aca5d3 100644 --- a/library/global.mli +++ b/library/global.mli @@ -14,7 +14,6 @@ open Entries open Indtypes open Mod_subst open Safe_typing - (**/**) (** This module defines the global environment of Coq. The functions below are exactly the same as the ones in [Safe_typing], operating on @@ -39,7 +38,7 @@ val env_is_empty : unit -> bool val push_named_assum : (identifier * types) -> Univ.constraints val push_named_def : (identifier * constr * types option) -> Univ.constraints -(** {6 Sect } *) +(** {6 ... } *) (** Adding constants, inductives, modules and module types. All these functions verify that given names match those generated by kernel *) @@ -94,7 +93,7 @@ val start_library : dir_path -> module_path val export : dir_path -> module_path * compiled_library val import : compiled_library -> Digest.t -> module_path -(** {6 Sect } *) +(** {6 ... } *) (** Function to get an environment from the constants part of the global * environment and a given context. *) diff --git a/library/impargs.mli b/library/impargs.mli index f43880e29..2eab1af66 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -12,8 +12,10 @@ open Term open Environ open Nametab -(** {6 Sect } *) -(** Implicit arguments. Here we store the implicit arguments. Notice that we +(** Implicit Arguments *) + +(** {6 ... } *) +(** Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit @@ -33,7 +35,7 @@ val is_maximal_implicit_args : unit -> bool type implicits_flags val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b -(** {6 Sect } *) +(** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) diff --git a/library/lib.mli b/library/lib.mli index f1e64e69a..5fb65a41f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -7,7 +7,8 @@ ***********************************************************************) -(** {6 Sect } *) +(** Lib: record of operations, backtrack, low-level sections *) + (** This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step). *) @@ -27,7 +28,7 @@ and library_segment = (Libnames.object_name * node) list type lib_objects = (Names.identifier * Libobject.obj) list -(** {6 Object iteratation functions. } *) +(** {6 Object iteration functions. } *) val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit @@ -47,7 +48,7 @@ val segment_of_objects : Libnames.object_prefix -> lib_objects -> library_segment -(** {6 Sect } *) +(** {6 ... } *) (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) @@ -71,7 +72,7 @@ val current_command_label : unit -> int registered after it. *) val reset_label : int -> unit -(** {6 Sect } *) +(** {6 ... } *) (** The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) diff --git a/library/libnames.mli b/library/libnames.mli index 9db6d787d..4e9ddcb56 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -120,7 +120,7 @@ val encode_con : dir_path -> identifier -> constant val decode_con : constant -> dir_path * identifier -(** {6 Sect } *) +(** {6 ... } *) (** A [qualid] is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial qualifications of absolute names, including single identifiers. @@ -161,7 +161,7 @@ type global_dir_reference = | DirClosedSection of dir_path (** this won't last long I hope! *) -(** {6 Sect } *) +(** {6 ... } *) (** A [reference] is the user-level notion of name. It denotes either a global name (referred either by a qualified name or by a single name) or a variable *) diff --git a/library/libobject.mli b/library/libobject.mli index 5a48419c9..87bbbe89d 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -84,7 +84,7 @@ val default_object : string -> 'a object_declaration (** the identity substitution function *) val ident_subst_function : substitution * 'a -> 'a -(** {6 Sect } *) +(** {6 ... } *) (** Given an object declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) diff --git a/library/library.mli b/library/library.mli index 9bbb45143..87e376ab9 100644 --- a/library/library.mli +++ b/library/library.mli @@ -11,7 +11,6 @@ open Names open Libnames open Libobject -(** {6 Sect } *) (** This module provides functions to load, open and save libraries. Libraries correspond to the subclass of modules that coincide with a file on disk (the ".vo" files). Libraries on the @@ -20,7 +19,7 @@ open Libobject written at various dates. *) -(** {6 Sect } *) +(** {6 ... } *) (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library : qualid located list -> bool option -> unit @@ -28,7 +27,7 @@ val require_library_from_dirpath : (dir_path * string) list -> bool option -> un val require_library_from_file : identifier option -> System.physical_path -> bool option -> unit -(** {6 Sect } *) +(** {6 ... } *) (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) val import_module : bool -> qualid located -> unit @@ -58,7 +57,7 @@ val overwrite_library_filenames : string -> unit (** {6 Hook for the xml exportation of libraries } *) val set_xml_require : (dir_path -> unit) -> unit -(** {6 Sect } *) +(** {6 ... } *) (** Global load paths: a load path is a physical path in the file system; to each load path is associated a Coq [dir_path] (the "logical" path of the physical path) *) diff --git a/library/nametab.mli b/library/nametab.mli index a464fd9a9..4303d86a3 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -11,51 +11,48 @@ open Pp open Names open Libnames -(** {6 Sect } *) -(** This module contains the tables for globalization, which - associates internal object references to qualified names (qualid). +(** This module contains the tables for globalization. *) - There are three classes of names: +(** These globalization tables associate internal object references to + qualified names (qualid). There are three classes of names: - 1a- internal kernel names: [kernel_name], [constant], [inductive], - [module_path], [dir_path] + - 1a) internal kernel names: [kernel_name], [constant], [inductive], + [module_path], [dir_path] - 1b- other internal names: [global_reference], [syndef_name], + - 1b) other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... - 2- full, non ambiguous user names: [full_path] + - 2) full, non ambiguous user names: [full_path] - 3- non necessarily full, possibly ambiguous user names: [reference] - and [qualid] + - 3) non necessarily full, possibly ambiguous user names: [reference] + and [qualid] *) (** Most functions in this module fall into one of the following categories: - {% \begin{%}itemize{% }%} - \item [push : visibility -> full_user_name -> object_reference -> unit] - - Registers the [object_reference] to be referred to by the - [full_user_name] (and its suffixes according to [visibility]). - [full_user_name] can either be a [full_path] or a [dir_path]. - - \item [exists : full_user_name -> bool] - - Is the [full_user_name] already atributed as an absolute user name - of some object? - - \item [locate : qualid -> object_reference] - - Finds the object referred to by [qualid] or raises [Not_found] - - \item [full_name : qualid -> full_user_name] - - Finds the full user name referred to by [qualid] or raises [Not_found] - - \item [shortest_qualid_of : object_reference -> user_name] - - The [user_name] can be for example the shortest non ambiguous [qualid] or - the [full_user_name] or [identifier]. Such a function can also have a - local context argument. - {% \end{%}itemize{% }%} +{ul {- [push : visibility -> full_user_name -> object_reference -> unit] + + Registers the [object_reference] to be referred to by the + [full_user_name] (and its suffixes according to [visibility]). + [full_user_name] can either be a [full_path] or a [dir_path]. + } + {- [exists : full_user_name -> bool] + + Is the [full_user_name] already atributed as an absolute user name + of some object? + } + {- [locate : qualid -> object_reference] + + Finds the object referred to by [qualid] or raises [Not_found] + } + {- [full_name : qualid -> full_user_name] + + Finds the full user name referred to by [qualid] or raises [Not_found] + } + {- [shortest_qualid_of : object_reference -> user_name] + + The [user_name] can be for example the shortest non ambiguous [qualid] or + the [full_user_name] or [identifier]. Such a function can also have a + local context argument.}} *) @@ -70,14 +67,12 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a (** {6 Register visibility of things } *) (** The visibility can be registered either - {% \begin{%}itemize{% }%} - \item for all suffixes not shorter then a given int -- when the - object is loaded inside a module -- or + - for all suffixes not shorter then a given int -- when the + object is loaded inside a module -- or - \item for a precise suffix, when the module containing (the module + - for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) - {% \end{%}itemize{% }%} *) type visibility = Until of int | Exactly of int @@ -138,7 +133,7 @@ val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path val full_name_module : qualid -> dir_path -(** {6 Sect } *) +(** {6 ... } *) (** Reverse lookup -- finding user names corresponding to the given internal name *) diff --git a/library/states.mli b/library/states.mli index f0dab29f2..9b5872bde 100644 --- a/library/states.mli +++ b/library/states.mli @@ -6,8 +6,9 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {6 Sect } *) -(** States of the system. In that module, we provide functions to get +(** {6 States of the system} *) + +(** In that module, we provide functions to get and set the state of the whole system. Internally, it is done by freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) @@ -19,14 +20,13 @@ type state val freeze : unit -> state val unfreeze : state -> unit -(** {6 Sect } *) -(** Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the +(** {6 Rollback } *) + +(** [with_heavy_rollback f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation if an exception is raised. *) - val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b -(** {6 Sect } *) (** [with_state_protection f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation of f *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 890aa005c..6184ed7a1 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -82,7 +82,8 @@ val lookup_path_to_sort_from : env -> evar_map -> types -> val lookup_pattern_path_between : inductive * inductive -> (constructor * int) list -(*i Crade *) +(**/**) +(* Crade *) open Pp val install_path_printer : ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 8ea91d28f..1ddf97c86 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -21,7 +21,8 @@ val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map val e_conv : env -> evar_map ref -> constr -> constr -> bool val e_cumul : env -> evar_map ref -> constr -> constr -> bool -(*i For debugging *) +(**/**) +(* For debugging *) val evar_conv_x : env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool val evar_eqappr_x : diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ebf91b4f4..43f214d0d 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -162,7 +162,7 @@ val is_evar : evar_map -> evar -> bool val is_defined : evar_map -> evar -> bool -(** {6 Sect } *) +(** {6 ... } *) (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has no body and [Not_found] if it does not exist in [sigma] *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index eba26bafe..18a6b03a7 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -81,8 +81,7 @@ sig val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment (**/**) - (** Internal of Pretyping... - *) + (** Internal of Pretyping... *) val pretype : type_constraint -> env -> evar_map ref -> var_map * (identifier * identifier option) list -> diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 78b01eeab..5651b7687 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -13,7 +13,9 @@ open Libnames open Libobject open Library -(** {6 Sect } *) +(** Operations concerning records and canonical structures *) + +(** {6 Records } *) (** A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) @@ -51,7 +53,7 @@ val methods_matching : constr -> ((global_reference*Evd.evar*Evd.evar_map) * (constr*existential_key)*Termops.subst) list -(** {6 Sect } *) +(** {6 Canonical structures } *) (** A canonical structure declares "canonical" conversion hints between the effective components of a structure and the projections of the structure *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9f3884088..5a0ba3cab 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -120,7 +120,7 @@ type meta_type_map = (metavariable * types) list (** [pop c] lifts by -1 the positive indexes in [c] *) val pop : constr -> constr -(** {6 Sect } *) +(** {6 ... } *) (** Substitution of an arbitrary large term. Uses equality modulo reduction of let *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 194dd1464..112003e8d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -23,7 +23,7 @@ open Tacexpr or [Theorem]), and ``goal'' means a subgoal of the current focused proof *) -(** {6 Sect } *) +(** {6 ... } *) (** [refining ()] tells if there is some proof in progress, even if a not focused one *) @@ -34,7 +34,7 @@ val refining : unit -> bool val check_no_pending_proofs : unit -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [delete_proof name] deletes proof of name [name] or fails if no proof has this name *) @@ -49,7 +49,7 @@ val delete_current_proof : unit -> unit val delete_all_proofs : unit -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [undo n] undoes the effect of the last [n] tactics applied to the current proof; it fails if no proof is focused or if the ``undo'' stack is exhausted *) @@ -69,7 +69,7 @@ val current_proof_depth: unit -> int val set_undo : int option -> unit val get_undo : unit -> int option -(** {6 Sect } *) +(** {6 ... } *) (** [start_proof s str env t hook tac] starts a proof of name [s] and conclusion [t]; [hook] is optionally a function to be applied at proof end (e.g. to declare the built constructions as a coercion @@ -89,7 +89,7 @@ val start_proof : val restart_proof : unit -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [resume_last_proof ()] focus on the last unfocused proof or fails if there is no suspended proofs *) @@ -105,7 +105,7 @@ val resume_proof : identifier located -> unit val suspend_proof : unit -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [cook_proof opacity] turns the current proof (assumed completed) into a constant with its name, kind and possible hook (see [start_proof]); it fails if there is no current proof of if it is not completed; @@ -119,7 +119,7 @@ val cook_proof : (Proof.proof -> unit) -> (** To export completed proofs to xml *) val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [get_Proof.proof ()] returns the current focused pending proof or raises [UserError "no focused proof"] *) @@ -140,7 +140,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env val current_proof_statement : unit -> identifier * goal_kind * types * declaration_hook -(** {6 Sect } *) +(** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) @@ -150,13 +150,13 @@ val get_current_proof_name : unit -> identifier val get_all_proof_names : unit -> identifier list -(** {6 Sect } *) +(** {6 ... } *) (** [set_end_tac tac] applies tactic [tac] to all subgoal generate by [solve_nth] *) val set_end_tac : tactic -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a UserError if no proof is focused or if there is no [n]th subgoal *) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 8def61112..b07389cee 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -65,7 +65,7 @@ type prim_rule = in the type of evar] \} \} \} v} *) -(** {6 Sect } *) +(** {6 ... } *) (** Proof trees. [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal diff --git a/tactics/auto.mli b/tactics/auto.mli index f7c3fd777..684478d96 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -20,6 +20,8 @@ open Libnames open Vernacexpr open Mod_subst +(** Auto and related automation tactics *) + type auto_tactic = | Res_pf of constr * clausenv (** Hint Apply *) | ERes_pf of constr * clausenv (** Hint EApply *) @@ -122,11 +124,11 @@ val make_apply_entry : -> hint_entry (** A constr which is Hint'ed will be: - (1) used as an Exact, if it does not start with a product - (2) used as an Apply, if its HNF starts with a product, and - has no missing arguments. - (3) used as an EApply, if its HNF starts with a product, and - has missing arguments. *) + - (1) used as an Exact, if it does not start with a product + - (2) used as an Apply, if its HNF starts with a product, and + has no missing arguments. + - (3) used as an EApply, if its HNF starts with a product, and + has missing arguments. *) val make_resolves : env -> evar_map -> bool * bool * bool -> int option -> constr -> diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 3fa8596f9..c44eb6fdd 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -14,7 +14,8 @@ open Evd open Pattern open Coqlib -(** {6 Sect } *) +(** High-order patterns *) + (** Given a term with second-order variables in it, represented by Meta's, and possibly applied using SoApp terms, this function will perform second-order, binding-preserving, @@ -34,7 +35,6 @@ open Coqlib intersection of the free-rels of the term and the current stack be contained in the arguments of the application *) -(** {6 Sect } *) (** I implemented the following functions which test whether a term [t] is an inductive but non-recursive type, a general conjuction, a general disjunction, or a type with no constructors. diff --git a/tactics/termdn.mli b/tactics/termdn.mli index ed3a928ab..dae4e8e30 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -64,5 +64,5 @@ sig val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option val constr_val_discr : constr -> (term_label * constr list) lookup_res -(**/**) + (**/**) end diff --git a/toplevel/command.mli b/toplevel/command.mli index 446cdc1b3..ab8329fb0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -19,18 +19,16 @@ open Redexpr open Constrintern open Pfedit -(** {6 Sect } *) (** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) -(** Hooks for Pcoq *) +(** {6 Hooks for Pcoq} *) val set_declare_definition_hook : (definition_entry -> unit) -> unit val get_declare_definition_hook : unit -> (definition_entry -> unit) val set_declare_assumptions_hook : (types -> unit) -> unit -(************************************************************************ - Definitions/Let *) +(** {6 Definitions/Let} *) val interp_definition : boxed_flag -> local_binder list -> red_expr option -> constr_expr -> @@ -39,8 +37,7 @@ val interp_definition : val declare_definition : identifier -> locality * definition_object_kind -> definition_entry -> manual_implicits -> declaration_hook -> unit -(************************************************************************ - Parameters/Assumptions *) +(** {6 Parameters/Assumptions} *) val interp_assumption : local_binder list -> constr_expr -> types * manual_implicits @@ -53,8 +50,7 @@ val declare_assumptions : variable located list -> coercion_flag -> assumption_kind -> types -> manual_implicits -> bool -> bool -> unit -(************************************************************************ - Inductive and coinductive types *) +(** {6 Inductive and coinductive types} *) (** Extracting the semantical components out of the raw syntax of mutual inductive declarations *) @@ -94,8 +90,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> bool -> unit -(************************************************************************ - Fixpoints and cofixpoints *) +(** {6 Fixpoints and cofixpoints} *) type structured_fixpoint_expr = { fix_name : identifier; diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 55d7dcf2e..6bc449d5b 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -34,7 +34,7 @@ val start_proof_with_initialization : (** A hook the next three functions pass to cook_proof *) val set_save_hook : (Proof.proof -> unit) -> unit -(** {6 Sect } *) +(** {6 ... } *) (** [save_named b] saves the current completed proof under the name it was started; boolean [b] tells if the theorem is declared opaque; it fails if the proof is not completed *) -- cgit v1.2.3