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.ml | 10 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/namegen.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 15 | ||||
| -rw-r--r-- | engine/proofview.mli | 3 | ||||
| -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 |
13 files changed, 43 insertions, 22 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ffff2c5dd9..111d0f3e8c 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 3ae6e586c1..df491c27b4 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 19041f1698..5db373199e 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 42e1e3784c..b70671a2d9 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.ml b/engine/logic_monad.ml index d67f1eee35..64be07b9c7 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -104,11 +104,11 @@ struct Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) - let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) - let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) + let print_debug s = make (fun _ -> Feedback.msg_info s) + let print_info s = make (fun _ -> Feedback.msg_info s) + let print_warning s = make (fun _ -> Feedback.msg_warning s) + let print_error s = make (fun _ -> Feedback.msg_error s) + let print_notice s = make (fun _ -> Feedback.msg_notice s) let run = fun x -> try x () with Exception e as src -> diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index c5160443b1..dd122cca0f 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 a2923fee99..e5c156b4e5 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.ml b/engine/proofview.ml index 95e20bc25a..bcdd4da115 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -46,7 +46,7 @@ let compact el ({ solution } as pv) = evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in - msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); + Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); new_el, { pv with solution = new_solution; } @@ -665,11 +665,12 @@ let with_shelf tac = (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) let goodmod p m = - let p' = p mod m in - (* if [n] is negative [n mod l] is negative of absolute value less - than [l], so [(n mod l)+l] is the representative of [n] in the - interval [[0,l-1]].*) - if p' < 0 then p'+m else p' + if m = 0 then 0 else + let p' = p mod m in + (* if [n] is negative [n mod l] is negative of absolute value less + than [l], so [(n mod l)+l] is the representative of [n] in the + interval [[0,l-1]].*) + if p' < 0 then p'+m else p' let cycle n = let open Proof in @@ -856,7 +857,7 @@ let tclTIME s t = else str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking") in - msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++ + Feedback.msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++ System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in let rec aux n t = let open Proof in diff --git a/engine/proofview.mli b/engine/proofview.mli index 7996b7969c..93ba55c61f 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -303,6 +303,9 @@ val guard_no_unifiable : Names.Name.t list option tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview +(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) +val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool + (** [with_shelf tac] executes [tac] and returns its result together with the set of goals shelved by [tac]. The current shelf is unchanged. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 0aff0a7207..637414cce7 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 643bea4036..aaf603efd8 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 c2a4f33235..76a31037bc 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 c5c454020c..0cdc6277a5 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 |