diff options
37 files changed, 75 insertions, 96 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 71127a92d..059b13c57 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4ff60578a..03ad950c7 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id$ i*) (*i*) open Names @@ -64,7 +64,7 @@ val interp_casted_openconstr : (* [interp_type_with_implicits] extends [interp_type] by allowing implicits arguments in the ``rel'' part of [env]; the extra argument associates a list of implicit positions to identifiers - declared in the rel_context of [env] *) + declared in the [rel_context] of [env] *) val interp_type_with_implicits : evar_map -> env -> full_implicits_env -> constr_expr -> types diff --git a/interp/coqlib.mli b/interp/coqlib.mli index fb4b2a423..6741e1a0a 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names @@ -80,7 +80,7 @@ val build_coq_eq_data : coq_leibniz_eq_data delayed val build_coq_eqT_data : coq_leibniz_eq_data delayed val build_coq_idT_data : coq_leibniz_eq_data delayed -val build_coq_eq : constr delayed (* = (build_coq_eq_data()).eq *) +val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) val build_coq_f_equal2 : constr delayed val build_coq_eqT : constr delayed val build_coq_sym_eqT : constr delayed diff --git a/interp/genarg.mli b/interp/genarg.mli index af02a9ebe..042520151 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Util open Names @@ -19,9 +19,9 @@ open Term type 'a or_var = ArgArg of 'a | ArgVar of identifier located type 'a and_short_name = 'a * identifier located option -(* In globalize tactics, we need to keep the initial constr_expr to recompute*) +(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) (* in the environment by the effective calls to Intro, Inversion, etc *) -(* The constr_expr field is None in TacDef though *) +(* The [constr_expr] field is [None] in TacDef though *) type rawconstr_and_expr = rawconstr * constr_expr option type open_constr = Evd.evar_map * Term.constr @@ -39,6 +39,7 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds (* The route of a generic argument, from parsing to evaluation +\begin{verbatim} parsing in_raw out_raw char stream ----> rawtype ----> rawconstr generic_argument ----> | @@ -46,16 +47,18 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds V type <---- constr generic_argument <---- out in +\end{verbatim} To distinguish between the uninterpreted (raw) and the interpreted -worlds, we annotate the type generic_argument by a phantom argument -which is either constr_expr or constr (actually we add also a second -argument raw_tactic_expr and tactic, but this is only for technical +worlds, we annotate the type [generic_argument] by a phantom argument +which is either [constr_expr] or [constr] (actually we add also a second +argument [raw_tactic_expr] and [tactic], but this is only for technical reasons, because these types are undefined at the type of compilation -of Genarg). +of [Genarg]). Transformation for each type : -tag f raw open type cooked closed type +\begin{verbatim} +tag raw open type cooked closed type BoolArgType bool bool IntArgType int int @@ -76,6 +79,7 @@ List0ArgType of argument_type List1ArgType of argument_type OptArgType of argument_type ExtraArgType of string '_a '_b +\end{verbatim} *) type ('a,'co,'ta) abstract_argument_type @@ -175,7 +179,7 @@ val wit_pair : ('b,'co,'ta) abstract_argument_type -> ('a * 'b,'co,'ta) abstract_argument_type -(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *) +(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) type ('a,'b) generic_argument val fold_list0 : @@ -255,7 +259,7 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a| - in_generic is not typable; we replace the second argument by an absurd + [in_generic] is not typable; we replace the second argument by an absurd type (with no introduction rule) *) type an_arg_of_this_type diff --git a/interp/notation.mli b/interp/notation.mli index e803d65e7..0e401acd6 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util @@ -30,7 +30,7 @@ open Ppextend type level = precedence * tolerability list type delimiters = string type scope -type scopes (* = scope_name list*) +type scopes (* = [scope_name list] *) val type_scope : scope_name val declare_scope : scope_name -> unit @@ -52,7 +52,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name (*s Declare and uses back and forth a numeral interpretation *) -(* A numeral interpreter is the pair of an interpreter for _integer_ +(* A numeral interpreter is the pair of an interpreter for **integer** numbers in terms and an optional interpreter in pattern, if negative numbers are not supported, the interpreter must fail with an appropriate error message *) @@ -69,12 +69,12 @@ type required_module = global_reference * string list val declare_numeral_interpreter : scope_name -> required_module -> num_interpreter -> num_uninterpreter -> unit -(* Returns the term/cases_pattern bound to a numeral in a given scope context*) +(* Return the [term]/[cases_pattern] bound to a numeral in a given scope context*) val interp_numeral : loc -> bigint -> scope_name list -> rawconstr val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list -> cases_pattern -(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *) +(* Return the numeral bound to a [term]/[cases_pattern]; raise [No_match] if no *) (* such numeral *) val uninterp_numeral : rawconstr -> scope_name * bigint val uninterp_cases_numeral : cases_pattern -> scope_name * bigint @@ -92,11 +92,11 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit -(* Returns the interpretation bound to a notation *) +(* Return the interpretation bound to a notation *) val interp_notation : loc -> notation -> scope_name list -> interpretation * ((dir_path * string) * scope_name option) -(* Returns the possible notations for a given term *) +(* Return the possible notations for a given term *) val uninterp_notations : rawconstr -> (interp_rule * interpretation * int option) list val uninterp_cases_pattern_notations : cases_pattern -> diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 68927dbad..bddd1eef2 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 4cfa0a0da..51fcd9c07 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp @@ -24,12 +24,12 @@ open Mod_subst (* non global expressions such as existential variables also *) type aconstr = - (* Part common to rawconstr and cases_pattern *) + (* Part common to [rawconstr] and [cases_pattern] *) | ARef of global_reference | AVar of identifier | AApp of aconstr * aconstr list | AList of identifier * identifier * aconstr * aconstr * bool - (* Part only in rawconstr *) + (* Part only in [rawconstr] *) | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr @@ -60,7 +60,7 @@ type scope_name = string type interpretation = (identifier * (scope_name option * scope_name list)) list * aconstr -val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation -> +val match_aconstr : rawconstr -> interpretation -> (rawconstr * (scope_name option * scope_name list)) list (*s Concrete syntax for terms *) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 30c0ffde0..3c99b67ac 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -33,7 +33,7 @@ type constant_body = { const_body : constr_substituted option; const_type : types; const_body_code : to_patch_substituted; - (* const_type_code : to_patch;*) + (*i const_type_code : to_patch;i*) const_constraints : constraints; const_opaque : bool } @@ -119,8 +119,8 @@ and module_specification_body = { msb_modtype : module_type_body; msb_equiv : module_path option; msb_constraints : constraints } - (* type_of(equiv) <: modtype (if given) - + substyping of past With_Module mergers *) + (* [type_of](equiv) <: modtype (if given) + + substyping of past [With_Module] mergers *) type structure_elem_body = @@ -136,7 +136,7 @@ and module_expr_body = | MEBfunctor of mod_bound_id * module_type_body * module_expr_body | MEBstruct of mod_self_id * module_structure_body | MEBapply of module_expr_body * module_expr_body (* (F A) *) - * constraints (* type_of(A) <: input_type_of(F) *) + * constraints (* [type_of](A) <: [input_type_of](F) *) and module_body = { mod_expr : module_expr_body option; @@ -144,7 +144,7 @@ and module_body = mod_type : module_type_body; mod_equiv : module_path option; mod_constraints : constraints } - (* type_of(mod_expr) <: mod_user_type (if given) *) + (* [type_of(mod_expr)] <: [mod_user_type] (if given) *) (* if equiv given then constraints are empty *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 5be23b490..20027d32a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,7 +46,7 @@ val engagement : env -> engagement option val empty_context : env -> bool (************************************************************************) -(*s Context of de Bruijn variables (rel_context) *) +(*s Context of de Bruijn variables ([rel_context]) *) val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 0174b8020..f419bc3fa 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -62,7 +62,7 @@ val type_case_branches : given inductive type. *) val check_case_info : env -> inductive -> case_info -> unit -(* Find the ultimate inductive in the mind_equiv chain *) +(* Find the ultimate inductive in the [mind_equiv] chain *) val scrape_mind : env -> mutual_inductive -> mutual_inductive diff --git a/kernel/modops.mli b/kernel/modops.mli index 052bac243..f102a5b2c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -42,7 +42,7 @@ val subst_signature_msid : module_signature_body -> module_signature_body (* [add_signature mp sign env] assumes that the substitution [msid] - \mapsto [mp] has already been performed (or is not necessary, like + $\mapsto$ [mp] has already been performed (or is not necessary, like when [mp = MPself msid]) *) val add_signature : module_path -> module_signature_body -> env -> env diff --git a/lib/bigint.mli b/lib/bigint.mli index 38de5b617..f363d536a 100644 --- a/lib/bigint.mli +++ b/lib/bigint.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/lib/rtree.mli b/lib/rtree.mli index 02112428c..80523d588 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -20,7 +20,7 @@ val mk_node : 'a -> 'a t array -> 'a t val mk_rec : 'a t array -> 'a t array (* [lift k t] increases of [k] the free parameters of [t]. Needed - to avoid captures when a tree appears under mk_rec *) + to avoid captures when a tree appears under [mk_rec] *) val lift : int -> 'a t -> 'a t val map : ('a -> 'b) -> 'a t -> 'b t diff --git a/library/declaremods.mli b/library/declaremods.mli index 17a97e7ae..5fce1fa48 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -84,7 +84,7 @@ val end_library : (* [really_import_module mp] opens the module [mp] (in a Caml sense). - It modifies Nametab and performs the "open_object" function for + It modifies Nametab and performs the [open_object] function for every object of the module. *) val really_import_module : module_path -> unit @@ -108,7 +108,7 @@ val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit val debug_print_modtab : unit -> Pp.std_ppcmds -(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*) +(*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*) (* For translator *) val process_module_bindings : module_ident list -> diff --git a/library/lib.mli b/library/lib.mli index fa8a34344..0433897ba 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -60,7 +60,7 @@ val add_leaf : identifier -> obj -> object_name val add_absolutely_named_leaf : object_name -> obj -> unit val add_anonymous_leaf : obj -> unit -(* this operation adds all objects with the same name and calls load_object +(* this operation adds all objects with the same name and calls [load_object] for each of them *) val add_leaves : identifier -> obj list -> object_name @@ -110,7 +110,7 @@ val start_modtype : module_ident -> module_path -> Summary.frozen -> object_prefix val end_modtype : module_ident -> object_name * object_prefix * Summary.frozen * library_segment -(* Lib.add_frozen_state must be called after each of the above functions *) +(* [Lib.add_frozen_state] must be called after each of the above functions *) (*s Compilation units *) diff --git a/library/libnames.mli b/library/libnames.mli index 379ce64b4..8d4ba269d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -111,8 +111,8 @@ val qualid_of_dirpath : dir_path -> qualid val make_short_qualid : identifier -> qualid -(* Both names are passed to objects: a "semantic" kernel_name, which - can be substituted and a "syntactic" section_path which can be printed +(* Both names are passed to objects: a "semantic" [kernel_name], which + can be substituted and a "syntactic" [section_path] which can be printed *) type object_name = section_path * kernel_name @@ -121,7 +121,7 @@ type object_prefix = dir_path * (module_path * dir_path) val make_oname : object_prefix -> identifier -> object_name -(* to this type are mapped dir_path's in the nametab *) +(* to this type are mapped [dir_path]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix diff --git a/library/libobject.mli b/library/libobject.mli index 562ba0ce4..37447ffbe 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -40,7 +40,7 @@ open Mod_subst Keep - the object is not substitutive, but survives module closing Anticipate - this is for objects which have to be explicitely - managed by the end_module function (like Require + managed by the [end_module] function (like Require and Read markers) The classification function is also an occasion for a cleanup diff --git a/library/nameops.mli b/library/nameops.mli index 257cedfbb..8dd2f6d74 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Names @@ -20,7 +20,7 @@ val make_ident : string -> int option -> identifier val repr_ident : identifier -> string * int option val atompart_of_id : identifier -> string (* remove trailing digits *) -val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *) +val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_$ *) val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier diff --git a/library/nametab.mli b/library/nametab.mli index bd6780c8a..81e7c6166 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -33,13 +33,14 @@ open Libnames \item [locate : qualid -> object_reference] - Finds the object referred to by [qualid] or raises Not_found + Finds the object referred to by [qualid] or raises [Not_found] - \item [name_of] : object_reference -> user_name + \item [name_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} *) @@ -155,7 +156,7 @@ val id_of_global : global_reference -> identifier val pr_global_env : Idset.t -> global_reference -> std_ppcmds -(* The [shortest_qualid] functions given an object with user_name +(* The [shortest_qualid] functions given an object with [user_name] Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes the same object. *) diff --git a/parsing/coqast.mli b/parsing/coqast.mli index b588d9cea..a083d09a6 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -42,9 +42,9 @@ val hcons_ast: * (kernel_name -> kernel_name) * (constant -> constant) -> (t -> t) * (loc -> loc) -(* +(*i val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr val fold_tactic_expr : ('a -> t -> 'a) -> ('a -> tactic_expr -> 'a) -> 'a -> tactic_expr -> 'a val iter_tactic_expr : (tactic_expr -> unit) -> tactic_expr -> unit -*) +i*) diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli index d6a7f4468..0344a27e2 100644 --- a/parsing/esyntax.mli +++ b/parsing/esyntax.mli @@ -48,16 +48,5 @@ module Ppprim : val declare_primitive_printer : string -> scope_name -> primitive_printer -> unit -(* -val declare_infix_symbol : Libnames.section_path -> string -> unit -*) - (* Generic printing functions *) -(* -val token_printer: std_printer -> std_printer -*) -(* -val print_syntax_entry : - string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds -*) val genprint : std_printer -> unparsing_subfunction diff --git a/parsing/extend.mli b/parsing/extend.mli index c9558a970..80a0e4448 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -113,11 +113,6 @@ type 'pat unparsing_hunk = | UNP_FNL | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk -(*val subst_unparsing_hunk : - substitution -> (substitution -> 'pat -> 'pat) -> - 'pat unparsing_hunk -> 'pat unparsing_hunk -*) - (* Checks if the precedence of the parent printer (None means the highest precedence), and the child's one, follow the given relation. *) diff --git a/parsing/printer.mli b/parsing/printer.mli index 01b691a13..8be938f81 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -24,9 +24,6 @@ open Proof_type (*i*) (* These are the entry points for printing terms, context, tac, ... *) -(* -val gentacpr : Tacexpr.raw_tactic_expr -> std_ppcmds -*) val prterm_env : env -> constr -> std_ppcmds val prterm_env_at_top : env -> constr -> std_ppcmds diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 3208bd593..2e8057cb0 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -36,7 +36,7 @@ type clausenv = { templval : constr freelisted; templtyp : constr freelisted } -(* Substitution is not applied on templenv (because subst_clenv is +(* Substitution is not applied on templenv (because [subst_clenv] is applied only on hints which typing env is overwritten by the goal env) *) val subst_clenv : substitution -> clausenv -> clausenv @@ -47,7 +47,7 @@ val clenv_value : clausenv -> constr val clenv_type : clausenv -> types (* substitute resolved metas *) val clenv_nf_meta : clausenv -> constr -> constr -(* type of a meta in clenvś context *) +(* type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types val mk_clenv_from : evar_info sigma -> constr * types -> clausenv @@ -67,7 +67,7 @@ val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv (***************************************************************) (* Unification with clenvs *) -(* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *) +(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) val clenv_unify : bool -> conv_pb -> constr -> constr -> clausenv -> clausenv @@ -75,7 +75,7 @@ val clenv_unify : val clenv_unique_resolver : bool -> clausenv -> evar_info sigma -> clausenv -(* same as above (allow_K=false) but replaces remaining metas +(* same as above ([allow_K=false]) but replaces remaining metas with fresh evars *) val evar_clenv_unique_resolver : clausenv -> evar_info sigma -> clausenv diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 2bc813678..7f18a7943 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Names open Term @@ -77,7 +77,7 @@ val make_arity_signature : val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types -(* Raise Not_found if not given an valid inductive type *) +(* Raise [Not_found] if not given an valid inductive type *) val extract_mrectype : constr -> inductive * constr list val find_mrectype : env -> evar_map -> constr -> inductive * constr list val find_rectype : env -> evar_map -> constr -> inductive_type diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 2b0b8f240..b4f6c3245 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -40,7 +40,7 @@ val is_matching : constr_pattern -> constr -> bool val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (* [match_subterm n pat c] returns the substitution and the context - corresponding to the [n+1]th _closed_ subterm of [c] matching [pat]; + corresponding to the [n+1]th **closed** subterm of [c] matching [pat]; It raises PatternMatchingFailure if no such matching exists *) val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 759e0adb6..b56e862ac 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -89,11 +89,11 @@ i*) val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr -(* +(*i val map_rawconstr_with_binders_loc : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr -*) +i*) val occur_rawconstr : identifier -> rawconstr -> bool diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index b7d8c1b85..423a04723 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -65,7 +65,7 @@ val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form - [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *) + [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *) val reduce_to_quantified_ref : env -> evar_map -> Libnames.global_reference -> types -> types diff --git a/pretyping/termops.mli b/pretyping/termops.mli index adc0e6daa..b290a5e5f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Util open Pp @@ -16,7 +16,6 @@ open Sign open Environ (* Universes *) -(*val set_module : Names.dir_path -> unit*) val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts val new_Type : unit -> types @@ -139,7 +138,7 @@ val named_hd_type : env -> types -> name -> name val mkProd_name : env -> name * types * types -> types val mkLambda_name : env -> name * types * constr -> constr -(* Deprecated synonyms of mkProd_name and mkLambda_name *) +(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) val prod_name : env -> name * types * types -> types val lambda_name : env -> name * types * constr -> constr diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 57312cb4b..090671e04 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -23,4 +23,4 @@ val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate -(* the instantiate tactic was moved to tactics/evar_tactics.ml *) +(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 3a0faa722..b21485e45 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,4 +1,3 @@ - (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 22b9de0b7..66cb97fac 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -119,9 +119,6 @@ val top_of_tree : pftreestate -> pftreestate val change_constraints_pftreestate : evar_map -> pftreestate -> pftreestate -(* -val vernac_tactic : string * tactic_arg list -> tactic -*) (*s The most primitive tactics. *) val refiner : rule -> tactic diff --git a/tactics/auto.mli b/tactics/auto.mli index 5c1959169..7442c34d3 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -106,7 +106,7 @@ val make_resolves : (* [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; - Never raises an User_exception; + Never raises a user exception; If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index f5b35e57d..dc547c2a8 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -80,9 +80,6 @@ val h_rename : identifier -> identifier -> tactic (* Constructors *) -(* -val h_any_constructor : tactic -> tactic -*) val h_constructor : int -> constr bindings -> tactic val h_left : constr bindings -> tactic val h_right : constr bindings -> tactic diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2fe4b7c6d..67dbcfc0f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -127,7 +127,7 @@ type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) -(* Useful for "as intro_pattern" modifier *) +(* Useful for [as intro_pattern] modifier *) val compute_induction_names : int -> intro_pattern_expr option -> intro_pattern_expr list array diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 418c3095f..b804de067 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -26,6 +26,7 @@ open Genarg open Tacexpr open Nametab open Rawterm +(*i*) (* Main tactics. *) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index da26f63f6..dc521cc55 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -27,11 +27,11 @@ val show_node : unit -> unit in the context of the current goal, as for instance in pcoq *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env +(*i (* this function is used to analyse the extra arguments in search commands. It is used in pcoq. *) (*i anciennement: inside_outside i*) -(* val interp_search_restriction : search_restriction -> dir_path list * bool -*) +i*) type pcoq_hook = { start_proof : unit -> unit; |