aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.mli8
-rw-r--r--engine/ftactic.mli4
-rw-r--r--engine/geninterp.mli3
-rw-r--r--engine/logic_monad.mli2
-rw-r--r--engine/namegen.mli2
-rw-r--r--engine/proofview_monad.mli3
-rw-r--r--engine/sigma.mli6
-rw-r--r--engine/termops.mli3
-rw-r--r--engine/uState.mli4
-rw-r--r--kernel/constr.mli3
-rw-r--r--kernel/names.mli14
-rw-r--r--lib/genarg.mli51
-rw-r--r--proofs/clenv.mli4
-rw-r--r--proofs/clenvtac.mli2
-rw-r--r--proofs/goal.mli4
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_type.mli27
-rw-r--r--proofs/proof_using.mli2
-rw-r--r--proofs/redexpr.mli2
-rw-r--r--proofs/refine.mli5
-rw-r--r--proofs/refiner.mli2
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/autorewrite.mli2
-rw-r--r--tactics/class_tactics.mli2
-rw-r--r--tactics/tactics.mli5
27 files changed, 93 insertions, 77 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ffff2c5dd..111d0f3e8 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -11,7 +11,7 @@ open Term
open Evd
open Environ
-(** {5 This modules provides useful functions for unification modulo evars } *)
+(** This module provides useful higher-level functions for evar manipulation. *)
(** {6 Metas} *)
diff --git a/engine/evd.mli b/engine/evd.mli
index 3ae6e586c..df491c27b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -12,7 +12,10 @@ open Names
open Term
open Environ
-(** {5 Existential variables and unification states}
+(** This file defines the pervasive unification state used everywhere in Coq
+ tactic engine. It is very low-level and most of the functions exported here
+ are irrelevant to the standard API user. Consider using {!Evarutil},
+ {!Sigma} or {!Proofview} instead.
A unification state (of type [evar_map]) is primarily a finite mapping
from existential variables to records containing the type of the evar
@@ -23,6 +26,8 @@ open Environ
It also contains conversion constraints, debugging information and
information about meta variables. *)
+(** {5 Existential variables and unification states} *)
+
(** {6 Evars} *)
type evar = existential_key
@@ -343,7 +348,6 @@ val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b
module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map
-
(** {5 Meta machinery}
These functions are almost deprecated. They were used before the
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 19041f169..5db373199 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -8,7 +8,9 @@
open Proofview.Notations
-(** Potentially focussing tactics *)
+(** This module defines potentially focussing tactics. They are used by Ltac to
+ emulate the historical behaviour of always-focussed tactics while still
+ allowing to remain global when the goal is not needed. *)
type +'a focus
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 42e1e3784..b70671a2d 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -6,7 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Interpretation functions for generic arguments. *)
+(** Interpretation functions for generic arguments and interpreted Ltac
+ values. *)
open Names
open Genarg
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index c5160443b..dd122cca0 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** This file defines the low-level monadic operations used by the
+(** This file implements the low-level monadic operations used by the
tactic monad. The monad is divided into two layers: a non-logical
layer which consists in operations which will not (or cannot) be
backtracked in case of failure (input/output or persistent state)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index a2923fee9..e5c156b4e 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file features facilities to generate fresh names. *)
+
open Names
open Term
open Environ
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 0aff0a720..637414cce 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -7,7 +7,8 @@
(************************************************************************)
(** This file defines the datatypes used as internal states by the
- tactic monad, and specialises the [Logic_monad] to these type. *)
+ tactic monad, and specialises the [Logic_monad] to these types. It should
+ not be used directly. Consider using {!Proofview} instead. *)
(** {6 Traces} *)
diff --git a/engine/sigma.mli b/engine/sigma.mli
index 643bea403..aaf603efd 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -12,7 +12,9 @@ open Constr
(** Monotonous state enforced by typing.
This module allows to constrain uses of evarmaps in a monotonous fashion,
- and in particular statically suppress evar leaks and the like.
+ and in particular statically suppress evar leaks and the like. To this
+ ends, it defines a type of indexed evarmaps whose phantom typing ensures
+ monotonous use.
*)
(** {5 Stages} *)
@@ -32,7 +34,7 @@ val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
(** {5 Monotonous evarmaps} *)
type 'r t
-(** Stage-indexed evarmaps. *)
+(** Stage-indexed evarmaps. This is just a plain evarmap with a phantom type. *)
type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
(** Return values at a later stage *)
diff --git a/engine/termops.mli b/engine/termops.mli
index c2a4f3323..76a31037b 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -6,6 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file defines various utilities for term manipulation that are not
+ needed in the kernel. *)
+
open Pp
open Names
open Term
diff --git a/engine/uState.mli b/engine/uState.mli
index c5c454020..0cdc6277a 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -6,7 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Universe unification states *)
+(** This file defines universe unification states which are part of evarmaps.
+ Most of the API below is reexported in {!Evd}. Consider using higher-level
+ primitives when needed. *)
open Names
diff --git a/kernel/constr.mli b/kernel/constr.mli
index f76b5ae4f..42d298e3b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -6,6 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file defines the most important datatype of Coq, namely kernel terms,
+ as well as a handful of generic manipulation functions. *)
+
open Names
(** {6 Value under universe substitution } *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 56f0f8c60..feaedc775 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,6 +6,20 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file defines a lot of different notions of names used pervasively in
+ the kernel as well as in other places. The essential datatypes exported by
+ this API are:
+
+ - Id.t is the type of identifiers, that is morally a subset of strings which
+ only contains Unicode characters of the Letter kind (and a few more).
+ - Name.t is an ad-hoc variant of Id.t option allowing to handle optionally
+ named objects.
+ - DirPath.t represents generic paths as sequences of identifiers.
+ - Label.t is an equivalent of Id.t made distinct for semantical purposes.
+ - ModPath.t are module paths.
+ - KerName.t are absolute names of objects in Coq.
+*)
+
open Util
(** {6 Identifiers } *)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index b8bb6af04..d7ad9b93b 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Generic arguments used by the extension mechanisms of several Coq ASTs. *)
+
(** The route of a generic argument, from parsing to evaluation.
In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
@@ -34,36 +36,10 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
effective use
{% \end{%}verbatim{% }%}
-To distinguish between the uninterpreted (raw), globalized and
+To distinguish between the uninterpreted, globalized and
interpreted worlds, we annotate the type [generic_argument] by a
-phantom argument which is either [constr_expr], [glob_constr] or
-[constr].
+phantom argument.
-Transformation for each type :
-{% \begin{%}verbatim{% }%}
-tag raw open type cooked closed type
-
-BoolArgType bool bool
-IntArgType int int
-IntOrVarArgType int or_var int
-StringArgType string (parsed w/ "") string
-PreIdentArgType string (parsed w/o "") (vernac only)
-IdentArgType true identifier identifier
-IdentArgType false identifier (pattern_ident) identifier
-IntroPatternArgType intro_pattern_expr intro_pattern_expr
-VarArgType identifier located identifier
-RefArgType reference global_reference
-QuantHypArgType quantified_hypothesis quantified_hypothesis
-ConstrArgType constr_expr constr
-ConstrMayEvalArgType constr_expr may_eval constr
-OpenConstrArgType open_constr_expr open_constr
-ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings
-BindingsArgType constr_expr bindings constr bindings
-List0ArgType of argument_type
-List1ArgType of argument_type
-OptArgType of argument_type
-ExtraArgType of string '_a '_b
-{% \end{%}verbatim{% }%}
*)
(** {5 Generic types} *)
@@ -77,14 +53,14 @@ sig
val name : string -> any option
end
+(** Generic types. The first parameter is the OCaml lowest level, the second one
+ is the globalized level, and third one the internalized level. *)
type (_, _, _) genarg_type =
| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
-(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
- one, and ['top] the internalized one. *)
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision when the three types agree. *)
@@ -99,21 +75,18 @@ val create_arg : string -> ('raw, 'glob, 'top) genarg_type
(** {5 Specialized types} *)
(** All of [rlevel], [glevel] and [tlevel] must be non convertible
- to ensure the injectivity of the type inference from type
- ['co generic_argument] to [('a,'co) abstract_argument_type];
- this guarantees that, for 'co fixed, the type of
- out_gen is monomorphic over 'a, hence type-safe
-*)
+ to ensure the injectivity of the GADT type inference. *)
type rlevel = [ `rlevel ]
type glevel = [ `glevel ]
type tlevel = [ `tlevel ]
+(** Generic types at a fixed level. The first parameter embeds the OCaml type
+ and the second one the level. *)
type (_, _) abstract_argument_type =
| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
-(** Type at level ['co] represented by an OCaml value of type ['a]. *)
type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
(** Specialized type at raw level. *)
@@ -207,9 +180,11 @@ sig
end
-(** {5 Basic generic type constructors} *)
+(** {5 Compatibility layer}
+
+The functions below are aliases for generic_type constructors.
-(** {6 Parameterized types} *)
+*)
val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 59b166ea0..e9236b1da 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,6 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file defines clausenv, which is a deprecated way to handle open terms
+ in the proof engine. Most of the API here is legacy except for the
+ evar-based clauses. *)
+
open Names
open Term
open Environ
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 00e74a247..aa091aecd 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Legacy components of the previous proof engine. *)
+
open Term
open Clenv
open Tacexpr
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 8a3d6e815..6a79c1f45 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -6,7 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* This module implements the abstract interface to goals *)
+(** This module implements the abstract interface to goals. Most of the code
+ here is useless and should be eventually removed. Consider using
+ {!Proofview.Goal} instead. *)
type goal = Evar.t
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9aa4ac207..2764d28c0 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Legacy proof engine. Do not use in newly written code. *)
+
open Names
open Term
open Evd
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index cfab8bd63..666730e1a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
+
open Loc
open Names
open Term
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ef0d52b62..f7798a0ed 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Legacy proof engine. Do not use in newly written code. *)
+
open Evd
open Names
open Term
@@ -26,31 +28,6 @@ type prim_rule =
type rule = prim_rule
-(** The type [goal sigma] is the type of subgoal. It has the following form
-{v it = \{ evar_concl = [the conclusion of the subgoal]
- evar_hyps = [the hypotheses of the subgoal]
- evar_body = Evar_Empty;
- evar_info = \{ pgm : [The Realizer pgm if any]
- lc : [Set of evar num occurring in subgoal] \}\}
- sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare]
- ed : [A set of existential variables depending in the subgoal]
- number of first evar,
- it = \{ evar_concl = [the type of first evar]
- evar_hyps = [the context of the evar]
- evar_body = [the body of the Evar if any]
- evar_info = \{ pgm : [Useless ??]
- lc : [Set of evars occurring
- in the type of evar] \} \};
- ...
- number of last evar,
- it = \{ evar_concl = [the type of evar]
- evar_hyps = [the context of the evar]
- evar_body = [the body of the Evar if any]
- evar_info = \{ pgm : [Useless ??]
- lc : [Set of evars occurring
- in the type of evar] \} \} \} v}
-*)
-
type goal = Goal.goal
type tactic = goal sigma -> goal list sigma
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index 1bf38b690..b2c65412f 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Utility code for section variables handling in Proof using... *)
+
val process_expr :
Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
Names.Id.t list
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index b91911087..d4c2c4a6c 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
+
open Names
open Term
open Pattern
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 17c7e28ca..a9798b704 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -6,6 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** The primitive refine tactic used to fill the holes in partial proofs. This
+ is the recommanded way to write tactics when the proof term is easy to
+ write down. Note that this is not the user-level refine tactic defined
+ in Ltac which is actually based on the one below. *)
+
open Proofview
(** {6 The refine tactic} *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index dd9153a02..6dcafb77a 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Legacy proof engine. Do not use in newly written code. *)
+
open Evd
open Proof_type
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 8c4f35904..0fd95aead 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This files implements auto and related automation tactics *)
+
open Names
open Term
open Clenv
@@ -13,8 +15,6 @@ open Pattern
open Decl_kinds
open Hints
-(** Auto and related automation tactics *)
-
val priority : ('a * full_hint) list -> ('a * full_hint) list
val default_search_depth : int ref
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index ac613b57c..070657179 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This files implements the autorewrite tactic. *)
+
open Term
open Tacexpr
open Equality
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index f1bcfa7dd..cac4b8844 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This files implements typeclasses eauto *)
+
open Names
open Constr
open Tacmach
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index df41951c3..fa7b6791e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -21,7 +21,10 @@ open Unification
open Misctypes
open Locus
-(** Main tactics. *)
+(** Main tactics defined in ML. This file is huge and should probably be split
+ in more reasonable units at some point. Because of its size and age, the
+ implementation features various styles and stages of the proof engine.
+ This has to be uniformized someday. *)
(** {6 General functions. } *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:45:47 +0000