diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.mli | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 8 | ||||
| -rw-r--r-- | engine/ftactic.mli | 4 | ||||
| -rw-r--r-- | engine/geninterp.mli | 3 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/namegen.mli | 2 | ||||
| -rw-r--r-- | engine/proofview_monad.mli | 3 | ||||
| -rw-r--r-- | engine/sigma.mli | 6 | ||||
| -rw-r--r-- | engine/termops.mli | 3 | ||||
| -rw-r--r-- | engine/uState.mli | 4 |
10 files changed, 27 insertions, 10 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 |