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 --- tactics/auto.mli | 77 ++++++++++++++++++++-------------------- tactics/autorewrite.mli | 24 ++++++------- tactics/btermdn.mli | 18 +++++----- tactics/contradiction.mli | 16 ++++----- tactics/dhyp.mli | 18 +++++----- tactics/dn.mli | 5 +-- tactics/eauto.mli | 18 +++++----- tactics/elim.mli | 18 +++++----- tactics/elimschemes.mli | 20 +++++------ tactics/eqschemes.mli | 22 ++++++------ tactics/evar_tactics.mli | 14 ++++---- tactics/extraargs.mli | 16 ++++----- tactics/extratactics.mli | 14 ++++---- tactics/hiddentac.mli | 32 ++++++++--------- tactics/hipattern.mli | 62 ++++++++++++++++---------------- tactics/inv.mli | 16 ++++----- tactics/nbtermdn.mli | 18 +++++----- tactics/refine.mli | 14 ++++---- tactics/tacinterp.mli | 54 ++++++++++++++-------------- tactics/tacticals.mli | 66 +++++++++++++++++----------------- tactics/tactics.mli | 90 +++++++++++++++++++++++------------------------ tactics/termdn.mli | 32 ++++++++--------- 22 files changed, 319 insertions(+), 345 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.mli b/tactics/auto.mli index 072e02989a..37fe3d4418 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* hint_db val searchtable_add : (hint_db_name * hint_db) -> unit -(* [create_hint_db local name st use_dn]. +(** [create_hint_db local name st use_dn]. [st] is a transparency state for unification using this db [use_dn] switches the use of the discrimination net for all hints and patterns. *) @@ -108,13 +106,13 @@ val print_hint_db_by_name : hint_db_name -> unit val print_hint_db : Hint_db.t -> unit -(* [make_exact_entry pri (c, ctyp)]. +(** [make_exact_entry pri (c, ctyp)]. [c] is the term given as an exact proof to solve the goal; [ctyp] is the type of [c]. *) val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry -(* [make_apply_entry (eapply,verbose) pri (c,cty)]. +(** [make_apply_entry (eapply,verbose) pri (c,cty)]. [eapply] is true if this hint will be used only with EApply; [hnf] should be true if we should expand the head of cty before searching for products; @@ -125,7 +123,7 @@ val make_apply_entry : env -> evar_map -> bool * bool * bool -> int option -> constr * constr -> hint_entry -(* A constr which is Hint'ed will be: +(** 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. @@ -136,7 +134,7 @@ val make_resolves : env -> evar_map -> bool * bool * bool -> int option -> constr -> hint_entry list -(* [make_resolve_hyp hname htyp]. +(** [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; Never raises a user exception; If the hyp cannot be used as a Hint, the empty list is returned. *) @@ -144,7 +142,7 @@ val make_resolves : val make_resolve_hyp : env -> evar_map -> named_declaration -> hint_entry list -(* [make_extern pri pattern tactic_expr] *) +(** [make_extern pri pattern tactic_expr] *) val make_extern : int -> constr_pattern option -> Tacexpr.glob_tactic_expr @@ -161,7 +159,7 @@ val set_extern_subst_tactic : (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) -> unit -(* Create a Hint database from the pairs (name, constr). +(** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) @@ -173,47 +171,47 @@ val default_search_depth : int ref val auto_unif_flags : Unification.unify_flags -(* Try unification with the precompiled clause, then use registered Apply *) +(** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve_nodelta : (constr * clausenv) -> tactic val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic -(* [ConclPattern concl pat tacast]: +(** [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic -(* The Auto tactic *) +(** The Auto tactic *) val auto : int -> constr list -> hint_db_name list -> tactic -(* Auto with more delta. *) +(** Auto with more delta. *) val new_auto : int -> constr list -> hint_db_name list -> tactic -(* auto with default search depth and with the hint database "core" *) +(** auto with default search depth and with the hint database "core" *) val default_auto : tactic -(* auto with all hint databases except the "v62" compatibility database *) +(** auto with all hint databases except the "v62" compatibility database *) val full_auto : int -> constr list -> tactic -(* auto with all hint databases except the "v62" compatibility database +(** auto with all hint databases except the "v62" compatibility database and doing delta *) val new_full_auto : int -> constr list -> tactic -(* auto with default search depth and with all hint databases +(** auto with default search depth and with all hint databases except the "v62" compatibility database *) val default_full_auto : tactic -(* The generic form of auto (second arg [None] means all bases) *) +(** The generic form of auto (second arg [None] means all bases) *) val gen_auto : int option -> constr list -> hint_db_name list option -> tactic -(* The hidden version of auto *) +(** The hidden version of auto *) val h_auto : int option -> constr list -> hint_db_name list option -> tactic -(* Trivial *) +(** Trivial *) val trivial : constr list -> hint_db_name list -> tactic val gen_trivial : constr list -> hint_db_name list option -> tactic val full_trivial : constr list -> tactic @@ -221,15 +219,16 @@ val h_trivial : constr list -> hint_db_name list option -> tactic val pr_autotactic : auto_tactic -> Pp.std_ppcmds -(*s The following is not yet up to date -- Papageno. *) +(** {6 The following is not yet up to date -- Papageno. } *) -(* DAuto *) +(** DAuto *) val dauto : int option * int option -> constr list -> tactic val default_search_decomp : int ref val default_dauto : tactic val h_dauto : int option * int option -> constr list -> tactic -(* SuperAuto *) + +(** SuperAuto *) type autoArguments = | UsingTDB diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index cf0d58ccb4..a9556891a6 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,34 +1,32 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* raw_rew_rule list -> unit -(* The AutoRewrite tactic. +(** The AutoRewrite tactic. The optional conditions tell rewrite how to handle matching and side-condition solving. Default is Naive: first match in the clause, don't look at the side-conditions to tell if the rewrite succeeded. *) val autorewrite : ?conds:conditions -> tactic -> string list -> tactic val autorewrite_in : ?conds:conditions -> Names.identifier -> tactic -> string list -> tactic -(* Rewriting rules *) +(** Rewriting rules *) type rew_rule = { rew_lemma: constr; rew_type: types; rew_pat: constr; diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index ebded23ac6..ebb046a05f 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,20 +1,18 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* sig diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 9c38362a8c..b5fdf5a1bc 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -1,20 +1,18 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic val contradiction : constr with_bindings option -> tactic diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 41fd497f7a..465a2a377e 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -1,20 +1,18 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic) -> unit diff --git a/tactics/dn.mli b/tactics/dn.mli index 3cb52a565f..662ac19afe 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -17,7 +17,7 @@ sig val create : unit -> t - (* [add t f (tree,inf)] adds a structured object [tree] together with + (** [add t f (tree,inf)] adds a structured object [tree] together with the associated information [inf] to the table [t]; the function [f] is used to translated [tree] into its prefix decomposition: [f] must decompose any tree into a label characterizing its root node and @@ -31,7 +31,8 @@ sig type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res -(* [lookup t f tree] looks for trees (and their associated + +(** [lookup t f tree] looks for trees (and their associated information) in table [t] such that the structured object [tree] matches against them; [f] is used to translated [tree] into its prefix decomposition: [f] must decompose any tree into a label diff --git a/tactics/eauto.mli b/tactics/eauto.mli index a5d1f0d375..595917bdff 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -1,12 +1,11 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic) -> branch_args -> tactic diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index fecf3e60da..ef1c4ec3e2 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -1,16 +1,16 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> inductive -> sorts_family -> constr -(* Builds a symmetry scheme for a symmetrical equality type *) +(** Builds a symmetry scheme for a symmetrical equality type *) val build_sym_scheme : env -> inductive -> constr val sym_scheme_kind : individual scheme_kind @@ -40,7 +40,7 @@ val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> constr val sym_involutive_scheme_kind : individual scheme_kind -(* Builds a congruence scheme for an equality type *) +(** Builds a congruence scheme for an equality type *) val congr_scheme_kind : individual scheme_kind val build_congr : env -> constr * constr -> inductive -> constr diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 2e30cdfbee..0cf4dbb809 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* identifier move_location -> tactic val h_intro : identifier -> tactic @@ -63,7 +61,7 @@ val h_generalize_dep : constr -> tactic val h_let_tac : letin_flag -> name -> constr -> Tacticals.clause -> tactic -(* Derived basic tactics *) +(** Derived basic tactics *) val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic @@ -84,17 +82,17 @@ val h_induction_destruct : rec_flag -> evars_flag -> val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic -(* Automation tactic : see Auto *) +(** Automation tactic : see Auto *) -(* Context management *) +(** Context management *) val h_clear : bool -> identifier list -> tactic val h_clear_body : identifier list -> tactic val h_move : bool -> identifier -> identifier move_location -> tactic val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic -(* Constructors *) +(** Constructors *) val h_constructor : evars_flag -> int -> constr bindings -> tactic val h_left : evars_flag -> constr bindings -> tactic val h_right : evars_flag -> constr bindings -> tactic @@ -105,12 +103,12 @@ val h_simplest_left : tactic val h_simplest_right : tactic -(* Conversion *) +(** Conversion *) val h_reduce : Redexpr.red_expr -> Tacticals.clause -> tactic val h_change : Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic -(* Equivalence relations *) +(** Equivalence relations *) val h_reflexivity : tactic val h_symmetry : Tacticals.clause -> tactic val h_transitivity : constr option -> tactic diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 9b04a2cd27..40ad0da9ba 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool val match_with_non_recursive_type : (constr * constr list) matching_function val is_non_recursive_type : testing_function -(* Non recursive type with no indices and exactly one argument for each +(** Non recursive type with no indices and exactly one argument for each constructor; canonical definition of n-ary disjunction if strict *) val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function val is_disjunction : ?strict:bool -> testing_function -(* Non recursive tuple (one constructor and no indices) with no inner +(** Non recursive tuple (one constructor and no indices) with no inner dependencies; canonical definition of n-ary conjunction if strict *) val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function val is_conjunction : ?strict:bool -> testing_function -(* Non recursive tuple, possibly with inner dependencies *) +(** Non recursive tuple, possibly with inner dependencies *) val match_with_record : (constr * constr list) matching_function val is_record : testing_function -(* Like record but supports and tells if recursive (e.g. Acc) *) +(** Like record but supports and tells if recursive (e.g. Acc) *) val match_with_tuple : (constr * constr list * bool) matching_function val is_tuple : testing_function -(* No constructor, possibly with indices *) +(** No constructor, possibly with indices *) val match_with_empty_type : constr matching_function val is_empty_type : testing_function -(* type with only one constructor and no arguments, possibly with indices *) +(** type with only one constructor and no arguments, possibly with indices *) val match_with_unit_or_eq_type : constr matching_function val is_unit_or_eq_type : testing_function -(* type with only one constructor and no arguments, no indices *) +(** type with only one constructor and no arguments, no indices *) val is_unit_type : testing_function -(* type with only one constructor, no arguments and at least one dependency *) +(** type with only one constructor, no arguments and at least one dependency *) val is_inductive_equality : inductive -> bool val match_with_equality_type : (constr * constr list) matching_function val is_equality_type : testing_function @@ -95,7 +95,7 @@ val is_forall_term : testing_function val match_with_imp_term : (constr * constr) matching_function val is_imp_term : testing_function -(* I added these functions to test whether a type contains dependent +(** I added these functions to test whether a type contains dependent products or not, and if an inductive has constructors with dependent types (excluding parameters). this is useful to check whether a conjunction is a real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002) *) @@ -109,7 +109,7 @@ val is_nodep_ind : testing_function val match_with_sigma_type : (constr * constr list) matching_function val is_sigma_type : testing_function -(* Recongnize inductive relation defined by reflexivity *) +(** Recongnize inductive relation defined by reflexivity *) type equation_kind = | MonomorphicLeibnizEq of constr * constr @@ -123,37 +123,37 @@ val match_with_equation: (***** Destructing patterns bound to some theory *) -(* Match terms [eq A t u], [identity A t u] or [JMeq A t A u] *) -(* Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) +(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] + Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) val find_eq_data_decompose : Proof_type.goal sigma -> constr -> coq_eq_data * (types * constr * constr) -(* Idem but fails with an error message instead of PatternMatchingFailure *) +(** Idem but fails with an error message instead of PatternMatchingFailure *) val find_this_eq_data_decompose : Proof_type.goal sigma -> constr -> coq_eq_data * (types * constr * constr) -(* A variant that returns more informative structure on the equality found *) +(** A variant that returns more informative structure on the equality found *) val find_eq_data : constr -> coq_eq_data * equation_kind -(* Match a term of the form [(existT A P t p)] *) -(* Returns associated lemmas and [A,P,t,p] *) +(** Match a term of the form [(existT A P t p)] + Returns associated lemmas and [A,P,t,p] *) val find_sigma_data_decompose : constr -> coq_sigma_data * (constr * constr * constr * constr) -(* Match a term of the form [{x:A|P}], returns [A] and [P] *) +(** Match a term of the form [{x:A|P}], returns [A] and [P] *) val match_sigma : constr -> constr * constr val is_matching_sigma : constr -> bool -(* Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns +(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : constr -> bool * constr * constr * constr * constr -(* Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) +(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) open Proof_type open Tacmach val dest_nf_eq : goal sigma -> constr -> (constr * constr * constr) -(* Match a negation *) +(** Match a negation *) val is_matching_not : constr -> bool val is_matching_imp_False : constr -> bool diff --git a/tactics/inv.mli b/tactics/inv.mli index 8ec0e2db24..a7780206ba 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* sig diff --git a/tactics/refine.mli b/tactics/refine.mli index 89e5316755..c9a4598e59 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Evd.evar_map -> Environ.env -> Pretyping.var_map * Pretyping.unbound_ltac_var_map -(* Transforms an id into a constr if possible *) +(** Transforms an id into a constr if possible *) val constr_of_id : Environ.env -> identifier -> constr -(* To embed several objects in Coqast.t *) +(** To embed several objects in Coqast.t *) val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr) @@ -58,19 +56,19 @@ val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr val valueIn : value -> raw_tactic_arg val constrIn : constr -> constr_expr -(* Sets the debugger mode *) +(** Sets the debugger mode *) val set_debug : debug_info -> unit -(* Gives the state of debug *) +(** Gives the state of debug *) val get_debug : unit -> debug_info -(* Adds a definition for tactics in the table *) +(** Adds a definition for tactics in the table *) val add_tacdef : Vernacexpr.locality_flag -> bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit -(* Tactic extensions *) +(** Tactic extensions *) val add_tactic : string -> (typed_generic_argument list -> tactic) -> unit val overwriting_add_tactic : @@ -78,7 +76,7 @@ val overwriting_add_tactic : val lookup_tactic : string -> (typed_generic_argument list) -> tactic -(* Adds an interpretation function for extra generic arguments *) +(** Adds an interpretation function for extra generic arguments *) type glob_sign = { ltacvars : identifier list * identifier list; ltacrecvars : (identifier * Nametab.ltac_constant) list; @@ -118,17 +116,17 @@ val subst_genarg : val subst_rawconstr_and_expr : substitution -> rawconstr_and_expr -> rawconstr_and_expr -(* Interprets any expression *) +(** Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value -(* Interprets an expression that evaluates to a constr *) +(** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> constr -(* Interprets redexp arguments *) +(** Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr -(* Interprets tactic expressions *) +(** Interprets tactic expressions *) val interp_tac_gen : (identifier * value) list -> identifier list -> debug_info -> raw_tactic_expr -> tactic @@ -136,7 +134,7 @@ val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings -(* Initial call for interpretation *) +(** Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr @@ -149,21 +147,21 @@ val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr -(* Hides interpretation for pretty-print *) +(** Hides interpretation for pretty-print *) val hide_interp : raw_tactic_expr -> tactic option -> tactic -(* Declare the default tactic to fill implicit arguments *) +(** Declare the default tactic to fill implicit arguments *) val declare_implicit_tactic : tactic -> unit -(* Declare the xml printer *) +(** Declare the xml printer *) val declare_xml_printer : (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit -(* printing *) +(** printing *) val print_ltac : Libnames.qualid -> std_ppcmds -(* Internals that can be useful for syntax extensions. *) +(** Internals that can be useful for syntax extensions. *) exception CannotCoerceTo of string diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 3dd73c92c3..c357451a21 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic -> tactic val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic -(*s Tacticals applying to hypotheses *) +(** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (identifier -> tactic) -> tactic val onNthHyp : int -> (constr -> tactic) -> tactic @@ -96,14 +94,14 @@ val ifOnHyp : (identifier * types -> bool) -> val onHyps : (goal sigma -> named_context) -> (named_context -> tactic) -> tactic -(*s Tacticals applying to goal components *) +(** {6 Tacticals applying to goal components } *) -(* A [simple_clause] is a set of hypotheses, possibly extended with +(** A [simple_clause] is a set of hypotheses, possibly extended with the conclusion (conclusion is represented by None) *) type simple_clause = identifier option list -(* A [clause] denotes occurrences and hypotheses in a +(** A [clause] denotes occurrences and hypotheses in a goal; in particular, it can abstractly refer to the set of hypotheses independently of the effective contents of the current goal *) @@ -126,21 +124,21 @@ val onAllHypsAndConclLR : (identifier option -> tactic) -> tactic val onClause : (identifier option -> tactic) -> clause -> tactic val onClauseLR : (identifier option -> tactic) -> clause -> tactic -(*s An intermediate form of occurrence clause with no mention of occurrences *) +(** {6 An intermediate form of occurrence clause with no mention of occurrences } *) -(* A [hyp_location] is an hypothesis together with a position, in +(** A [hyp_location] is an hypothesis together with a position, in body if any, in type or in both *) type hyp_location = identifier * hyp_location_flag -(* A [goal_location] is either an hypothesis (together with a position, in +(** A [goal_location] is either an hypothesis (together with a position, in body if any, in type or in both) or the goal *) type goal_location = hyp_location option -(*s A concrete view of occurrence clauses *) +(** {6 A concrete view of occurrence clauses } *) -(* [clause_atom] refers either to an hypothesis location (i.e. an +(** [clause_atom] refers either to an hypothesis location (i.e. an hypothesis with occurrences and a position, in body if any, in type or in both) or to some occurrences of the conclusion *) @@ -148,40 +146,40 @@ type clause_atom = | OnHyp of identifier * occurrences_expr * hyp_location_flag | OnConcl of occurrences_expr -(* A [concrete_clause] is an effective collection of +(** A [concrete_clause] is an effective collection of occurrences in the hypotheses and the conclusion *) type concrete_clause = clause_atom list -(* This interprets an [clause] in a given [goal] context *) +(** This interprets an [clause] in a given [goal] context *) val concrete_clause_of : clause -> goal sigma -> concrete_clause -(*s Elimination tacticals. *) +(** {6 Elimination tacticals. } *) type branch_args = { - ity : inductive; (* the type we were eliminating on *) - largs : constr list; (* its arguments *) - branchnum : int; (* the branch number *) - pred : constr; (* the predicate we used *) - nassums : int; (* the number of assumptions to be introduced *) - branchsign : bool list; (* the signature of the branch. + ity : inductive; (** the type we were eliminating on *) + largs : constr list; (** its arguments *) + branchnum : int; (** the branch number *) + pred : constr; (** the predicate we used *) + nassums : int; (** the number of assumptions to be introduced *) + branchsign : bool list; (** the signature of the branch. true=recursive argument, false=constant *) branchnames : intro_pattern_expr located list} type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) + ba : branch_args; (** the branch args *) + assums : named_context} (** the list of assumptions introduced *) -(* [check_disjunctive_pattern_size loc pats n] returns an appropriate *) -(* error message if |pats| <> n *) +(** [check_disjunctive_pattern_size loc pats n] returns an appropriate + error message if |pats| <> n *) val check_or_and_pattern_size : Util.loc -> or_and_intro_pattern_expr -> int -> unit -(* Tolerate "[]" to mean a disjunctive pattern of any length *) +(** Tolerate "[]" to mean a disjunctive pattern of any length *) val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> or_and_intro_pattern_expr -(* Useful for [as intro_pattern] modifier *) +(** Useful for [as intro_pattern] modifier *) val compute_induction_names : int -> intro_pattern_expr located option -> intro_pattern_expr located list array diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0e552bd408..2d7c074029 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string val head_constr : constr -> constr * constr list @@ -42,7 +40,7 @@ val is_quantified_hypothesis : identifier -> goal sigma -> bool exception Bound -(*s Primitive tactics. *) +(** {6 Primitive tactics. } *) val introduction : identifier -> tactic val refine : constr -> tactic @@ -55,7 +53,7 @@ val fix : identifier option -> int -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic val cofix : identifier option -> tactic -(*s Introduction tactics. *) +(** {6 Introduction tactics. } *) val fresh_id_in_env : identifier list -> identifier -> env -> identifier val fresh_id : identifier list -> identifier -> goal sigma -> identifier @@ -65,7 +63,7 @@ val intro : tactic val introf : tactic val intro_move : identifier option -> identifier move_location -> tactic - (* [intro_avoiding idl] acts as intro but prevents the new identifier + (** [intro_avoiding idl] acts as intro but prevents the new identifier to belong to [idl] *) val intro_avoiding : identifier list -> tactic @@ -78,7 +76,7 @@ val intros_replacing : identifier list -> tactic val intros : tactic -(* [depth_of_quantified_hypothesis b h g] returns the index of [h] in +(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : bool -> quantified_hypothesis -> goal sigma -> int @@ -88,7 +86,7 @@ val intros_until : quantified_hypothesis -> tactic val intros_clearing : bool list -> tactic -(* Assuming a tactic [tac] depending on an hypothesis identifier, +(** Assuming a tactic [tac] depending on an hypothesis identifier, [try_intros_until tac arg] first assumes that arg denotes a quantified hypothesis (denoted by name or by index) and try to introduce it in context before to apply [tac], otherwise assume the @@ -97,21 +95,21 @@ val intros_clearing : bool list -> tactic val try_intros_until : (identifier -> tactic) -> quantified_hypothesis -> tactic -(* Apply a tactic on a quantified hypothesis, an hypothesis in context +(** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) val onInductionArg : (constr with_bindings -> tactic) -> constr with_bindings induction_arg -> tactic -(*s Introduction tactics with eliminations. *) +(** {6 Introduction tactics with eliminations. } *) val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic val intro_patterns : intro_pattern_expr located list -> tactic val intros_pattern : identifier move_location -> intro_pattern_expr located list -> tactic -(*s Exact tactics. *) +(** {6 Exact tactics. } *) val assumption : tactic val exact_no_check : constr -> tactic @@ -119,7 +117,7 @@ val vm_cast_no_check : constr -> tactic val exact_check : constr -> tactic val exact_proof : Topconstr.constr_expr -> tactic -(*s Reduction tactics. *) +(** {6 Reduction tactics. } *) type tactic_reduction = env -> evar_map -> constr -> constr @@ -156,7 +154,7 @@ val pattern_option : val reduce : red_expr -> clause -> tactic val unfold_constr : global_reference -> tactic -(*s Modification of the local context. *) +(** {6 Modification of the local context. } *) val clear : identifier list -> tactic val clear_body : identifier list -> tactic @@ -169,7 +167,7 @@ val rename_hyp : (identifier * identifier) list -> tactic val revert : identifier list -> tactic -(*s Resolution tactics. *) +(** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> tactic val apply_term : constr -> constr list -> tactic @@ -193,7 +191,7 @@ val apply_in : val simple_apply_in : identifier -> constr -> tactic -(*s Elimination tactics. *) +(** {6 Elimination tactics. } *) (* @@ -219,36 +217,36 @@ val simple_apply_in : identifier -> constr -> tactic Principles taken from functional induction have the final (f...). *) -(* [rel_contexts] and [rel_declaration] actually contain triples, and +(** [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - index: int; (* index of the elimination type in the scheme *) - params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) - nparams: int; (* number of parameters *) - predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) - npredicates: int; (* Number of predicates *) - branches: rel_context; (* branchr,...,branch1 *) - nbranches: int; (* Number of branches *) - args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) - nargs: int; (* number of arguments *) - indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) + index: int; (** index of the elimination type in the scheme *) + params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (** number of parameters *) + predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (** Number of predicates *) + branches: rel_context; (** branchr,...,branch1 *) + nbranches: int; (** Number of branches *) + args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (** number of arguments *) + indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) - concl: types; (* Qi x1...xni HI (f...), HI and (f...) + concl: types; (** Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive *) - indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) - farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) + indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) + farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) } val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme val rebuild_elimtype_from_scheme: elim_scheme -> types -(* elim principle with the index of its inductive arg *) +(** elim principle with the index of its inductive arg *) type eliminator = { - elimindex : int option; (* None = find it automatically *) + elimindex : int option; (** None = find it automatically *) elimbody : constr with_bindings } @@ -278,7 +276,7 @@ val new_induct : evars_flag -> constr with_bindings induction_arg list -> intro_pattern_expr located option * intro_pattern_expr located option -> clause option -> tactic -(*s Case analysis tactics. *) +(** {6 Case analysis tactics. } *) val general_case_analysis : evars_flag -> constr with_bindings -> tactic val simplest_case : constr -> tactic @@ -289,7 +287,7 @@ val new_destruct : evars_flag -> constr with_bindings induction_arg list -> intro_pattern_expr located option * intro_pattern_expr located option -> clause option -> tactic -(*s Generic case analysis / induction tactics. *) +(** {6 Generic case analysis / induction tactics. } *) val induction_destruct : rec_flag -> evars_flag -> (constr with_bindings induction_arg list * @@ -298,12 +296,12 @@ val induction_destruct : rec_flag -> evars_flag -> list * clause option -> tactic -(*s Eliminations giving the type instead of the proof. *) +(** {6 Eliminations giving the type instead of the proof. } *) val case_type : constr -> tactic val elim_type : constr -> tactic -(*s Some eliminations which are frequently used. *) +(** {6 Some eliminations which are frequently used. } *) val impE : identifier -> tactic val andE : identifier -> tactic @@ -313,7 +311,7 @@ val dAnd : clause -> tactic val dorE : bool -> clause ->tactic -(*s Introduction tactics. *) +(** {6 Introduction tactics. } *) val constructor_tac : evars_flag -> int option -> int -> constr bindings -> tactic @@ -332,7 +330,7 @@ val simplest_left : tactic val simplest_right : tactic val simplest_split : tactic -(*s Logical connective tactics. *) +(** {6 Logical connective tactics. } *) val register_setoid_reflexivity : tactic -> unit val reflexivity_red : bool -> tactic @@ -368,7 +366,7 @@ val pose_proof : name -> constr -> tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic -val generalize_dep : ?with_let:bool (* Don't lose let bindings *) -> constr -> tactic +val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic val resolve_classes : tactic diff --git a/tactics/termdn.mli b/tactics/termdn.mli index aea49b0735..973cc0e5b6 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -1,25 +1,23 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t - (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) + (** [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) val add : t -> transparent_state -> (constr_pattern * Z.t) -> t val rmv : t -> transparent_state -> (constr_pattern * Z.t) -> t - (* [lookup t c] looks for patterns (with their action) matching term [c] *) + (** [lookup t c] looks for patterns (with their action) matching term [c] *) val lookup : t -> transparent_state -> constr -> (constr_pattern * Z.t) list val app : ((constr_pattern * Z.t) -> unit) -> t -> unit - (*i*) - (* These are for Nbtermdn *) + (**/**) + (** These are for Nbtermdn *) type term_label = | GRLabel of global_reference @@ -68,5 +66,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 -(*i*) +(**/**) end -- cgit v1.2.3