aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.mli77
-rw-r--r--tactics/autorewrite.mli24
-rw-r--r--tactics/btermdn.mli18
-rw-r--r--tactics/contradiction.mli16
-rw-r--r--tactics/dhyp.mli18
-rw-r--r--tactics/dn.mli5
-rw-r--r--tactics/eauto.mli18
-rw-r--r--tactics/elim.mli18
-rw-r--r--tactics/elimschemes.mli20
-rw-r--r--tactics/eqschemes.mli22
-rw-r--r--tactics/evar_tactics.mli14
-rw-r--r--tactics/extraargs.mli16
-rw-r--r--tactics/extratactics.mli14
-rw-r--r--tactics/hiddentac.mli32
-rw-r--r--tactics/hipattern.mli62
-rw-r--r--tactics/inv.mli16
-rw-r--r--tactics/nbtermdn.mli18
-rw-r--r--tactics/refine.mli14
-rw-r--r--tactics/tacinterp.mli54
-rw-r--r--tactics/tacticals.mli66
-rw-r--r--tactics/tactics.mli90
-rw-r--r--tactics/termdn.mli32
22 files changed, 319 insertions, 345 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 072e02989..37fe3d441 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Util
open Names
open Term
@@ -22,29 +21,28 @@ open Evd
open Libnames
open Vernacexpr
open Mod_subst
-(*i*)
type auto_tactic =
- | Res_pf of constr * clausenv (* Hint Apply *)
- | ERes_pf of constr * clausenv (* Hint EApply *)
+ | Res_pf of constr * clausenv (** Hint Apply *)
+ | ERes_pf of constr * clausenv (** Hint EApply *)
| Give_exact of constr
- | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *)
- | Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *)
+ | Res_pf_THEN_trivial_fail of constr * clausenv (** Hint Immediate *)
+ | Unfold_nth of evaluable_global_reference (** Hint Unfold *)
+ | Extern of Tacexpr.glob_tactic_expr (** Hint Extern *)
open Rawterm
type pri_auto_tactic = {
- pri : int; (* A number between 0 and 4, 4 = lower priority *)
- pat : constr_pattern option; (* A pattern for the concl of the Goal *)
- code : auto_tactic; (* the tactic to apply when the concl matches pat *)
+ pri : int; (** A number between 0 and 4, 4 = lower priority *)
+ pat : constr_pattern option; (** A pattern for the concl of the Goal *)
+ code : auto_tactic; (** the tactic to apply when the concl matches pat *)
}
type stored_data = pri_auto_tactic
type search_entry
-(* The head may not be bound. *)
+(** The head may not be bound. *)
type hint_entry = global_reference option * pri_auto_tactic
@@ -85,7 +83,7 @@ val searchtable_map : hint_db_name -> 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 cf0d58ccb..a9556891a 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -1,34 +1,32 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Term
open Tacexpr
open Tacmach
open Equality
-(*i*)
-(* Rewriting rules before tactic interpretation *)
+(** Rewriting rules before tactic interpretation *)
type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr
-(* To add rewriting rules to a base *)
+(** To add rewriting rules to a base *)
val add_rew_rules : string -> 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 ebded23ac..ebb046a05 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Term
open Pattern
open Names
-(*i*)
-(* Discrimination nets with bounded depth. *)
+(** Discrimination nets with bounded depth. *)
module Make :
functor (Z : Map.OrderedType) ->
sig
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 9c38362a8..b5fdf5a1b 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
open Proof_type
open Rawterm
open Genarg
-(*i*)
val absurd : constr -> tactic
val contradiction : constr with_bindings option -> tactic
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 41fd497f7..465a2a377 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Tacmach
open Tacexpr
-(*i*)
-(* Programmable destruction of hypotheses and conclusions. *)
+(** Programmable destruction of hypotheses and conclusions. *)
val set_extern_interp : (glob_tactic_expr -> tactic) -> unit
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 3cb52a565..662ac19af 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 a5d1f0d37..595917bdf 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -1,12 +1,11 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i*)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
+
open Term
open Proof_type
open Tacexpr
@@ -15,7 +14,6 @@ open Topconstr
open Evd
open Environ
open Explore
-(*i*)
val hintbases : hint_db_name list option Pcoq.Gram.Entry.e
val wit_hintbases : hint_db_name list option typed_abstract_argument_type
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 25ae07000..7fbb16ba1 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -1,23 +1,21 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
open Proof_type
open Tacmach
open Genarg
open Tacticals
-(*i*)
-(* Eliminations tactics. *)
+(** Eliminations tactics. *)
val introElimAssumsThen :
(branch_assumptions -> tactic) -> branch_args -> tactic
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index fecf3e60d..ef1c4ec3e 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -1,16 +1,16 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
-(* $Id$ *)
+(** {% $ %}Id: elimschemes.mli 12584 2009-12-13 21:04:34Z herbelin {% $ %} *)
open Ind_tables
-(* Induction/recursion schemes *)
+(** Induction/recursion schemes *)
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
@@ -20,7 +20,7 @@ val ind_dep_scheme_kind_from_type : individual scheme_kind
val rec_dep_scheme_kind_from_type : individual scheme_kind
-(* Case analysis schemes *)
+(** Case analysis schemes *)
val case_scheme_kind_from_type : individual scheme_kind
val case_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index a6ffe9e21..bdf3bbe76 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -1,21 +1,21 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(* This file builds schemes relative to equality inductive types *)
+(** This file builds schemes relative to equality inductive types *)
open Names
open Term
open Environ
open Ind_tables
-(* Builds a left-to-right rewriting scheme for an equality type *)
+(** Builds a left-to-right rewriting scheme for an equality type *)
val rew_l2r_dep_scheme_kind : individual scheme_kind
val rew_l2r_scheme_kind : individual scheme_kind
@@ -32,7 +32,7 @@ val build_l2r_forward_rew_scheme :
val build_r2l_forward_rew_scheme :
bool -> 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 2e30cdfbe..0cf4dbb80 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 4492fd842..3421ded92 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
@@ -51,7 +51,7 @@ val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
-(* Spiwack: Primitive for retroknowledge registration *)
+(** Spiwack: Primitive for retroknowledge registration *)
val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e
val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 82006f602..259fe8814 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 36b0830dd..dae0281bd 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -1,15 +1,14 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Util
open Term
@@ -21,12 +20,11 @@ open Rawterm
open Evd
open Clenv
open Termops
-(*i*)
-(* Tactics for the interpreter. They left a trace in the proof tree
+(** Tactics for the interpreter. They left a trace in the proof tree
when they are called. *)
-(* Basic tactics *)
+(** Basic tactics *)
val h_intro_move : identifier option -> 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 9b04a2cd2..40ad0da9b 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Util
open Names
open Term
@@ -16,9 +15,9 @@ open Sign
open Evd
open Pattern
open Coqlib
-(*i*)
-(*s Given a term with second-order variables in it,
+(** {6 Sect } *)
+(** 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,
matching, in the case where the pattern is a pattern in the sense
@@ -37,7 +36,8 @@ open Coqlib
intersection of the free-rels of the term and the current stack be
contained in the arguments of the application *)
-(*s I implemented the following functions which test whether a term [t]
+(** {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.
@@ -52,36 +52,36 @@ type testing_function = constr -> 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 8ec0e2db2..a7780206b 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Util
open Names
open Term
@@ -16,7 +15,6 @@ open Tacmach
open Genarg
open Tacexpr
open Rawterm
-(*i*)
type inversion_status = Dep of constr option | NoDep
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 027ea5734..3f866d5da 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Term
open Pattern
open Libnames
-(*i*)
-(* Named, bounded-depth, term-discrimination nets. *)
+(** Named, bounded-depth, term-discrimination nets. *)
module Make :
functor (Y:Map.OrderedType) ->
sig
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 89e531675..c9a4598e5 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 71ee29f8c..771d28fba 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Pp
open Util
open Names
@@ -21,9 +20,8 @@ open Genarg
open Topconstr
open Mod_subst
open Redexpr
-(*i*)
-(* Values for interpretation *)
+(** Values for interpretation *)
type value =
| VRTactic of (goal list sigma)
| VFun of ltac_trace * (identifier*value) list *
@@ -36,7 +34,7 @@ type value =
| VList of value list
| VRec of (identifier*value) list ref * glob_tactic_expr
-(* Signature for interpretation: val\_interp and interpretation functions *)
+(** Signature for interpretation: val\_interp and interpretation functions *)
and interp_sign =
{ lfun : (identifier * value) list;
avoid_ids : identifier list;
@@ -46,10 +44,10 @@ and interp_sign =
val extract_ltac_vars : interp_sign -> 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 3dd73c92c..c357451a2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Pp
open Util
open Names
@@ -23,9 +22,8 @@ open Genarg
open Tacexpr
open Termops
open Rawterm
-(*i*)
-(* Tacticals i.e. functions from tactics to tactics. *)
+(** Tacticals i.e. functions from tactics to tactics. *)
val tclNORMEVAR : tactic
val tclIDTAC : tactic
@@ -68,7 +66,7 @@ val tclIFTHENTRYELSEMUST : tactic -> 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 0e552bd40..2d7c07402 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Util
open Names
open Term
@@ -29,11 +28,10 @@ open Nametab
open Rawterm
open Pattern
open Termops
-(*i*)
-(* Main tactics. *)
+(** Main tactics. *)
-(*s General functions. *)
+(** {6 General functions. } *)
val string_of_inductive : constr -> 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 aea49b073..973cc0e5b 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -1,25 +1,23 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Term
open Pattern
open Libnames
open Names
-(*i*)
-(* Discrimination nets of terms. *)
+(** Discrimination nets of terms. *)
-(* This module registers actions (typically tactics) mapped to patterns *)
+(** This module registers actions (typically tactics) mapped to patterns *)
-(* Patterns are stocked linearly as the list of its node in prefix
+(** Patterns are stocked linearly as the list of its node in prefix
order in such a way patterns having the same prefix have this common
prefix shared and the seek for the action associated to the patterns
that a term matches are found in time proportional to the maximal
@@ -38,21 +36,21 @@ sig
val create : unit -> 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 04:56:25 +0000