diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 2 | ||||
| -rw-r--r-- | engine/evarutil.mli | 2 | ||||
| -rw-r--r-- | engine/ftactic.ml | 4 | ||||
| -rw-r--r-- | engine/ftactic.mli | 12 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 8 | ||||
| -rw-r--r-- | engine/proofview.mli | 4 | ||||
| -rw-r--r-- | engine/proofview_monad.ml | 2 | ||||
| -rw-r--r-- | engine/proofview_monad.mli | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 6 | ||||
| -rw-r--r-- | engine/univMinim.ml | 2 |
11 files changed, 26 insertions, 20 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 0a5bba39b9..7c2ecca89e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -860,7 +860,7 @@ let compare_constructor_instances evd u u' = [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8eaff8bd13..907be8eba2 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -208,7 +208,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns diff --git a/engine/ftactic.ml b/engine/ftactic.ml index dab2e7d5ef..b59d04e813 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -18,8 +18,8 @@ type 'a focus = (** Type of tactics potentially goal-dependent. If it contains a [Depends], then the length of the inner list is guaranteed to be the number of - currently focussed goals. Otherwise it means the tactic does not depend - on the current set of focussed goals. *) + currently focused goals. Otherwise it means the tactic does not depend + on the current set of focused goals. *) type 'a t = 'a focus Proofview.tactic let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index ed95d62bc6..5922781d4d 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -18,7 +18,7 @@ type +'a t = 'a focus Proofview.tactic (** The type of focussing tactics. A focussing tactic is like a normal tactic, except that it is able to remember it have entered a goal. Whenever this is the case, each subsequent effect of the tactic is dispatched on the - focussed goals. This is a monad. *) + focused goals. This is a monad. *) (** {5 Monadic interface} *) @@ -32,20 +32,20 @@ val bind : 'a t -> ('a -> 'b t) -> 'b t val lift : 'a Proofview.tactic -> 'a t (** Transform a tactic into a focussing tactic. The resulting tactic is not - focussed. *) + focused. *) val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** Given a continuation producing a tactic, evaluates the focussing tactic. If - the tactic has not focussed, then the continuation is evaluated once. - Otherwise it is called in each of the currently focussed goals. *) + the tactic has not focused, then the continuation is evaluated once. + Otherwise it is called in each of the currently focused goals. *) (** {5 Focussing} *) -(** Enter a goal. The resulting tactic is focussed. *) +(** Enter a goal. The resulting tactic is focused. *) val enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is - focussed. *) + focused. *) val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index e0c24f049f..a504ee28e2 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -151,7 +151,7 @@ struct (** Double-continuation backtracking monads are reasonable folklore for "search" implementations (including the Tac interactive prover's tactics). Yet it's quite hard to wrap your head around - these. I recommand reading a few times the "Backtracking, + these. I recommend reading a few times the "Backtracking, Interleaving, and Terminating Monad Transformers" paper by O. Kiselyov, C. Shan, D. Friedman, and A. Sabry. The peculiar shape of the monadic type is reminiscent of that of the diff --git a/engine/proofview.ml b/engine/proofview.ml index 5c5a02d3fa..c00c90e5e9 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -31,7 +31,7 @@ type entry = (EConstr.constr * EConstr.types) list ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) let proofview p = @@ -114,7 +114,7 @@ type focus_context = goal_with_state list * goal_with_state list instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) let focus_context (left,right) = @@ -123,7 +123,7 @@ let focus_context (left,right) = (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the - original list. The focused list has lenght [j-i-1] and contains + original list. The focused list has length [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises [IndexOutOfRange] if [i > length l], or [j > length l] or [j < @@ -245,7 +245,7 @@ let tclUNIT = Proof.return (** Bind operation of the tactic monad. *) let tclBIND = Proof.(>>=) -(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation, +(** Interprets the ";" (semicolon) of Ltac. As a monadic operation, it's a specialized "bind". *) let tclTHEN = Proof.(>>) diff --git a/engine/proofview.mli b/engine/proofview.mli index b7ff3ac432..60697c1611 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -24,7 +24,7 @@ type proofview ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) val proofview : proofview -> Evar.t list * Evd.evar_map @@ -95,7 +95,7 @@ type focus_context instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) val focus_context : focus_context -> Evar.t list * Evar.t list diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 80eb9d0124..8ed75a8d00 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -252,7 +252,7 @@ module Giveup : Writer with type t = goal list = struct let put gs = Logical.put (true, gs) end -(** Lens and utilies pertaining to the info trace *) +(** Lens and utilities pertaining to the info trace *) module InfoL = struct let recording = Logical.(map (fun {P.trace} -> trace) current) let if_recording t = diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 3437b6ce77..f0c9fdb589 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -145,7 +145,7 @@ module Shelf : State with type t = goal list of the tactic. *) module Giveup : Writer with type t = goal list -(** Lens and utilies pertaining to the info trace *) +(** Lens and utilities pertaining to the info trace *) module InfoL : sig (** [record_trace t] behaves like [t] and compute its [info] trace. *) val record_trace : 'a Logical.t -> 'a Logical.t diff --git a/engine/termops.ml b/engine/termops.ml index fcacb53ac4..05bb42ac61 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -306,9 +306,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma = let pr_evar_list env sigma l = let open Evd in + let pr_restrict ev = + match is_restricted_evar sigma ev with + | None -> mt () + | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")" + in let pr (ev, evi) = h 0 (Evar.print ev ++ str "==" ++ pr_evar_info env sigma evi ++ + pr_restrict ev ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) diff --git a/engine/univMinim.ml b/engine/univMinim.ml index fcbf305f9d..4f9f9ce6a5 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -353,7 +353,7 @@ let normalize_context_set g ctx us algs weak = noneqs Constraint.empty in (* Compute the left and right set of flexible variables, constraints - mentionning other variables remain in noneqs. *) + mentioning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> let lus = LMap.mem l us and rus = LMap.mem r us in |