diff options
73 files changed, 123 insertions, 123 deletions
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index 6efc8ec1fe..6bbf83aa7e 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -88,7 +88,7 @@ Cons: Makefiles hierarchy ------------------- +------------------- The Makefile is separated in several files : @@ -101,7 +101,7 @@ The Makefile is separated in several files : FIND_SKIP_DIRS ---------------- +-------------- The recommended style of using FIND_SKIP_DIRS is for example 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/gramlib/grammar.ml b/gramlib/grammar.ml index c452c7b307..f9d18e7190 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -222,7 +222,7 @@ let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) t | Stoken _, _ -> true | _ -> false -(** Ancilliary datatypes *) +(** Ancillary datatypes *) type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml index 251e3dded3..4c66a6944e 100644 --- a/ide/configwin_types.ml +++ b/ide/configwin_types.ml @@ -87,7 +87,7 @@ type modifiers_param = { (** The value, as a list of modifiers and a key code *) md_editable : bool ; (** indicates if the value can be changed *) md_f_apply : Gdk.Tags.modifier list -> unit ; - (** the function to call to apply the new value of the paramter *) + (** the function to call to apply the new value of the parameter *) md_help : string option ; (** optional help string *) md_expand : bool ; (** expand or not *) md_allow : Gdk.Tags.modifier list diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index ccb6bedaf6..9d8fdf6335 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -34,7 +34,7 @@ type status = { status_path : string list; (** Module path of the current proof *) status_proofname : string option; - (** Current proof name. [None] if no focussed proof is in progress *) + (** Current proof name. [None] if no focused proof is in progress *) status_allproofs : string list; (** List of all pending proofs. Order is not significant *) status_proofnum : int; @@ -43,7 +43,7 @@ type status = { type 'a pre_goals = { fg_goals : 'a list; - (** List of the focussed goals *) + (** List of the focused goals *) bg_goals : ('a list * 'a list) list; (** Zipper representing the unfocused background goals *) shelved_goals : 'a list; @@ -70,7 +70,7 @@ type option_state = { opt_sync : bool; (** Whether an option is synchronous *) opt_depr : bool; - (** Wheter an option is deprecated *) + (** Whether an option is deprecated *) opt_name : string; (** A short string that is displayed when using [Test] *) opt_value : option_value; diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli index 31fc7b56f1..18d4b1eeee 100644 --- a/ide/protocol/richpp.mli +++ b/ide/protocol/richpp.mli @@ -25,7 +25,7 @@ type 'annotation located = { of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired - annotation. [width] sets the printing witdh of the formatter. *) + annotation. [width] sets the printing width of the formatter. *) val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli index 178f7c808f..4b47aa9f7c 100644 --- a/ide/protocol/xml_printer.mli +++ b/ide/protocol/xml_printer.mli @@ -16,11 +16,11 @@ type target = TChannel of out_channel | TBuffer of Buffer.t val make : target -> t (** Print the xml data structure to a source into a compact xml string (without - any user-readable formating ). *) + any user-readable formatting ). *) val print : t -> xml -> unit (** Print the xml data structure into a compact xml string (without - any user-readable formating ). *) + any user-readable formatting ). *) val to_string : xml -> string (** Print the xml data structure into an user-readable string with diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index e18219210f..5b37ca35ed 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -405,7 +405,7 @@ end = struct | (lg, rg) :: l -> Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in - Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals + Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb66658a37..fe50bd4b08 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -107,7 +107,7 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 753065b7dd..31f3736bae 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); - (* Two possibilities: either the args are given with explict + (* Two possibilities: either the args are given with explicit variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be added later on; or the args are not enough to have all arguments, @@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with @returns a raw_case_pattern_expr : - no notations and syntactic definition - - global reference and identifeir instead of reference + - global reference and identifier instead of reference *) @@ -1642,7 +1642,7 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supportted only in local binders and only at top + are supported only in local binders and only at top level. In fact, they are currently eliminated by the parser. The only reason why they are in the [cases_pattern_expr] type is that the parser needs to factor diff --git a/interp/declare.mli b/interp/declare.mli index 2ffde31fc0..795d9a767d 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -40,7 +40,7 @@ type internal_flag = | InternalTacticRequest | UserIndividualRequest -(* Defaut definition entries, transparent with no secctx or proj information *) +(* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 806fe93297..f3cdd64633 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -96,11 +96,11 @@ let set_maximality imps b = this kind if there is enough arguments to infer them) - [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) - [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) diff --git a/interp/impargs.mli b/interp/impargs.mli index ccdd448460..1099074c63 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) + of a reference can be automatically inferred *) type argument_position = @@ -50,11 +50,11 @@ type implicit_explanation = this kind if there is enough arguments to infer them) *) | DepFlex of argument_position (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 49273c4146..a7e1de736c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = match onlyparse with | None -> (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) + notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat | _ -> () end diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 542a05fd25..a1c49bee95 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */ init_coq_interpreter(); /* Some predefined pointer code. - * It is typically contained in accumlator blocks whose tag is 0 and thus + * It is typically contained in accumulator blocks whose tag is 0 and thus * scanned by the GC, so make it look like an OCaml block. */ value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95f88c0306..fc7d1a54f2 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -226,7 +226,7 @@ let unfold_red kn = * this constant or abstraction. * * i_tab is the cache table of the results * - * ref_value_cache searchs in the tab, otherwise uses i_repr to + * ref_value_cache searches in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't * be unfolded, returns None, but does not store this failure. * This * doesn't take the RESET into account. You mustn't keep such a table @@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with and comp_subs el s = Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s -(* This function defines the correspondance between constr and +(* This function defines the correspondence between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1a790eaed6..60185464c5 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 69f004307d..90fbcb8ae3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -386,7 +386,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation *) +(* Extension of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function diff --git a/kernel/constr.mli b/kernel/constr.mli index 7fc57cdb8a..aa5878c9d7 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci]. - [p] stucture is [fun args x -> "return clause"] + [p] structure is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 36ee952099..860d19fe26 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -22,11 +22,11 @@ type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives - and constants hiding inductives are implicitely polymorphic when + and constants hiding inductives are implicitly polymorphic when applied to parameters, on the universes appearing in the whnf of their parameters and their conclusion, in a template style. - In truely universe polymorphic mode, we always use RegularArity. + In truly universe polymorphic mode, we always use RegularArity. *) type template_arity = { diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d9335d39b5..ca7086a3e4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -166,7 +166,7 @@ let make_subst env = (* template, it is identity substitution otherwise (ie. when u is *) (* already in the domain of the substitution) [remember_subst] will *) (* update its image [x] by [sup x u] in order not to forget the *) - (* dependency in [u] that remains to be fullfilled. *) + (* dependency in [u] that remains to be fulfilled. *) make (remember_subst u subst) (sign, exp, []) | _sign, [], _ -> (* Uniform parameters are exhausted *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 2de5faa6df..72393d0081 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = in let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature - with the identity substitution accompagned by the new resolver*) + with the identity substitution accompanied by the new resolver*) let id_subst = map_mp mp' mp' new_mb.mod_delta in let new_after = subst_structure id_subst after in before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst diff --git a/kernel/modops.ml b/kernel/modops.ml index 4fdd7ab334..472fddb829 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = "Module M:=P." or "Module M. Include P. End M." We need to perform two operations to compute the body of M. - The first one is applying the substitution {P <- M} on the type of P - - The second one is strenghtening. *) + - The second one is strengthening. *) let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with |NoFunctor struc -> diff --git a/kernel/uint63.mli b/kernel/uint63.mli index f25f24512d..93632da110 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -13,7 +13,7 @@ val of_uint : int -> t val hash : t -> int - (* convertion to a string *) + (* conversion to a string *) val to_string : t -> string val of_string : string -> t diff --git a/kernel/univ.ml b/kernel/univ.ml index b1bbc25fe6..2b88d6884d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -726,7 +726,7 @@ let univ_level_rem u v min = | Some u' -> if Level.equal u u' then min else v | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v -(* Is u mentionned in v (or equals to v) ? *) +(* Is u mentioned in v (or equals to v) ? *) (**********************************************************************) diff --git a/kernel/univ.mli b/kernel/univ.mli index db178c4bb0..ddb204dd52 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t val universe_level : Universe.t -> Level.t option -(** [univ_level_mem l u] Is l is mentionned in u ? *) +(** [univ_level_mem l u] Is l is mentioned in u ? *) val univ_level_mem : Level.t -> Universe.t -> bool diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 777a207013..5e3a3c3347 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -12,7 +12,7 @@ open Univ open Constr (*******************************************) -(* Initalization of the abstract machine ***) +(* Initialization of the abstract machine ***) (* Necessary for [relaccu_tbl] *) (*******************************************) diff --git a/lib/cProfile.mli b/lib/cProfile.mli index 764faf8d1a..00babe1a47 100644 --- a/lib/cProfile.mli +++ b/lib/cProfile.mli @@ -18,7 +18,7 @@ To trace a function "f" you first need to get a key for it by using : let fkey = declare_profile "f";; -(the string is used to print the profile infomation). Warning: this +(the string is used to print the profile information). Warning: this function does a side effect. Choose the ident you want instead "fkey". Then if the function has ONE argument add the following just after diff --git a/lib/envars.mli b/lib/envars.mli index ebf86d0650..558fe74042 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -38,7 +38,7 @@ val datadir : unit -> string (** [configdir] is the path to the installed config directory. *) val configdir : unit -> string -(** [set_coqlib] must be runned once before any access to [coqlib] *) +(** [set_coqlib] must be run once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) diff --git a/lib/feedback.mli b/lib/feedback.mli index f407e2fd5b..c9e6ca1266 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -56,7 +56,7 @@ type feedback = { (** {6 Feedback sent, even asynchronously, to the user interface} *) -(* The interpreter assignes an state_id to the ast, and feedbacks happening +(* The interpreter assigns a state_id to the ast, and feedbacks happening * during interpretation are attached to it. *) diff --git a/lib/flags.mli b/lib/flags.mli index a70a23b902..535b46950e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,7 +64,7 @@ val beautify : bool ref val beautify_file : bool ref (* Coq quiet mode. Note that normal mode is called "verbose" here, - whereas [quiet] supresses normal output such as goals in coqtop *) + whereas [quiet] suppresses normal output such as goals in coqtop *) val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b diff --git a/lib/pp.mli b/lib/pp.mli index 4ce6a535c8..8b3a07d4b2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -18,7 +18,7 @@ (* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned againt its use, *) +(* uses, however regular users are _strongly_ warned against its use, *) (* they should instead rely on the available functions below. *) (* *) (* Box order and number is indeed an important factor. Try to create *) diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 03468271d2..0eec18bd5a 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -88,7 +88,7 @@ Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight. -Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*". diff --git a/lib/spawn.mli b/lib/spawn.mli index 944aa27a7f..24bbded4f1 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -9,7 +9,7 @@ (************************************************************************) (* This module implements spawning/killing managed processes with a - * synchronous or asynchronous comunication channel that works with + * synchronous or asynchronous communication channel that works with * threads or with a glib like main loop model. * * This module requires no threads and no main loop model. It takes care diff --git a/library/declaremods.ml b/library/declaremods.ml index 5fd11e187a..d74bdd484c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -51,7 +51,7 @@ let inl2intopt = function - Then comes either the object segment itself (for interactive modules), or a compact way to store derived objects (path to - a earlier module + subtitution). + a earlier module + substitution). *) type algebraic_objects = diff --git a/library/library.ml b/library/library.ml index 500e77f89b..d8eaf5f659 100644 --- a/library/library.ml +++ b/library/library.ml @@ -208,7 +208,7 @@ let register_open_library export m = let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentionned by the user are always reopen *) + (* Libraries explicitly mentioned by the user are always reopen *) List.exists (fun m' -> DirPath.equal m m') explicit_libs || not (library_is_opened m) then begin @@ -347,7 +347,7 @@ let try_locate_absolute_library dir = (** {6 Tables of opaque proof terms} *) (** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, we can quickly load a first half of a .vo file without these opaque terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) diff --git a/library/nametab.mli b/library/nametab.mli index a4f177aad0..33cb4faf99 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -38,7 +38,7 @@ open Globnames } {- [exists : full_user_name -> bool] - Is the [full_user_name] already atributed as an absolute user name + Is the [full_user_name] already attributed as an absolute user name of some object? } {- [locate : qualid -> object_reference] diff --git a/library/summary.mli b/library/summary.mli index 0d77d725ac..3875bcfe9e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,7 +28,7 @@ type 'a summary_declaration = { Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence - the responsability of plugins to initialize themselves properly. + the responsibility of plugins to initialize themselves properly. *) val declare_summary : string -> 'a summary_declaration -> unit diff --git a/man/coqdep.1 b/man/coqdep.1 index c417402c25..4639a75677 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -106,7 +106,7 @@ Skips subdirectory Output the given file name ordered by dependencies. .TP .B \-boot -For coq developpers, prints dependencies over coq library files +For coq developers, prints dependencies over coq library files (omitted by default). diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8f38e437b4..a78ad4f842 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -585,7 +585,7 @@ let unfreeze (grams, lex) = (** No need to provide an init function : the grammar state is statically available, and already empty initially, while - the lexer state should not be resetted, since it contains + the lexer state should not be reset, since it contains keywords declared in g_*.ml4 *) let parser_summary_tag = diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index 4bc3dba36e..bc7e1448f7 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -200,7 +200,7 @@ For the moment there are: Wf.well_founded_induction Wf.well_founded_induction_type Those constants does not match the auto-inlining criterion based on strictness. -Of course, you can still overide this behaviour via some Extraction NoInline. +Of course, you can still override this behaviour via some Extraction NoInline. * There is now a web page showing the extraction of all standard theories: http://www.lri.fr/~letouzey/extraction diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 36bb1148b6..02da168fd0 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -(** Restore lazyness of andb, orb. +(** Restore laziness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined - by extraction in order to have lazyness, producing inelegant + by extraction in order to have laziness, producing inelegant (if ... then ... else false) and (if ... then true else ...). *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 59c57cc544..f46d09e335 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -573,7 +573,7 @@ let pp_ocaml_gen k mp rls olab = if is_mp_bound base then pp_ocaml_bound base rls else pp_ocaml_extern k base rls -(* For Haskell, things are simplier: we have removed (almost) all structures *) +(* For Haskell, things are simpler: we have removed (almost) all structures *) let pp_haskell_gen k mp rls = match rls with | [] -> assert false @@ -590,7 +590,7 @@ let pp_global k r = let s = List.hd ls in let mp,l = repr_of_r r in if ModPath.equal mp (top_visible_mp ()) then - (* simpliest situation: definition of r (or use in the same context) *) + (* simplest situation: definition of r (or use in the same context) *) (* we update the visible environment *) (add_visible (k,s) l; unquote s) else @@ -607,7 +607,7 @@ let pp_module mp = let ls = mp_renaming mp in match mp with | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) -> - (* simpliest situation: definition of mp (or use in the same context) *) + (* simplest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in add_visible (Mod,s) l; s diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d7bb27f121..db1a389fe7 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY -(* Same, with content splitted in several files *) +(* Same, with content split in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] -> { separate_extraction l } END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4e229a94b6..c2c48f9565 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -101,7 +101,7 @@ let labels_of_ref r = (*S The main tables: constants, inductives, records, ... *) -(* Theses tables are not registered within coq save/undo mechanism +(* These tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum @@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj = ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + declare_object @@ superglobal_object_nodischarge "ML extractions custom matches" ~cache:(fun (_,(r,s)) -> add_custom_match r s) ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 287a374ab1..cffe8a3e78 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -658,7 +658,7 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = *) (fun g -> -(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *) +(* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) thin [hid] g ) ) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e9a2c285d0..f51c6dc6be 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -429,11 +429,11 @@ let get_funs_constant mp = let l_const = get_funs_constant const f in (* We need to check that all the functions found are in the same block - to prevent Reset stange thing + to prevent Reset strange thing *) let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in - (* all the paremeter must be equal*) + (* all the parameters must be equal*) let _check_params = let first_params = List.hd l_params in List.iter @@ -514,7 +514,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ ) fas in - (* We create the first priciple by tactic *) + (* We create the first principle by tactic *) let first_type,other_princ_types = match l_schemes with s::l_schemes -> s,l_schemes diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e15e167ff3..4c67d65816 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1369,7 +1369,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in @@ -1438,7 +1438,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 481a8be3ba..24b3690138 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -55,7 +55,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr Glob_term.cases_pattern * Id.Map.key list * Id.t Id.Map.t -(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt +(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result respects barendregt conventions and does not share bound variables with avoid *) val alpha_rt : Id.t list -> glob_constr -> glob_constr diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 40f66ce5eb..48cf040919 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -115,7 +115,7 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (*****************************************************************) -(* Copy of the standart save mechanism but without the much too *) +(* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) open Entries @@ -357,7 +357,7 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) -(* Debuging *) +(* Debugging *) let functional_induction_rewrite_dependent_proofs = ref true let function_debug = ref false open Goptions diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index edb698280f..2a0140f02c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -591,7 +591,7 @@ let rec reflexivity_with_destruct_cases g = (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] - is the tactic used to prove completness lemma. + is the tactic used to prove completeness lemma. [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. @@ -748,7 +748,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let env = Global.env () in @@ -928,7 +928,7 @@ let revert_graph kn post_tac hid g = [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct] is the correctness lemma for [fconst]. - The sketch is the follwing~: + The sketch is the following~: \begin{enumerate} \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ (fails if it is not possible) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1fca132655..216be3797b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1584,7 +1584,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let pstate = com_terminate tcc_lemma_name diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 963b7189f9..f772da69a4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -207,7 +207,7 @@ end) = struct let mk_relation env evd a = app_poly env evd relation [| a |] - (** Build an infered signature from constraints on the arguments and expected output + (** Build an inferred signature from constraints on the arguments and expected output relation *) let build_signature evars env m (cstrs : (types * types option) option list) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 0eb7726a18..8bd69dd4fd 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index fd303f5d94..f839c3e886 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 800be2565d..4a0b01bcdc 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) - (* a name intented to be used as a (non-variable) identifier *) + (* a name intended to be used as a (non-variable) identifier *) try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id @@ -2075,7 +2075,7 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* EJGA: We sould also pass the proof name if desired, for now + (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) let name, poly = Id.of_string "ltac_gen", poly in diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 2b5e496168..7783661787 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index e0e2232be5..7759bda7c7 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -129,7 +129,7 @@ Proof. intros n m H1 H2; rewrite H2 in H1; now apply H1. Qed. -(* Propeties of plus, minus and opp *) +(* Properties of plus, minus and opp *) Theorem Rplus_0_l : forall n : R, 0 + n == n. Proof. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 60931df517..c5e179fbb8 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -990,7 +990,7 @@ Proof. rewrite IHs. reflexivity. Qed. -(** equality migth be (too) strong *) +(** equality might be (too) strong *) Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). Proof. destruct f. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index bed9e55ac0..48027442b2 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1208,8 +1208,8 @@ let dump_rexpr = lazy (** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occuring in form - - props is an environment for the propositions occuring in form + - vars is an environment for the arithmetic variables occurring in form + - props is an environment for the propositions occurring in form @return a goal where all the variables and propositions of the formula are quantified *) @@ -1469,7 +1469,7 @@ let pre_processZ mt f = x <= y or (x and y are incomparable) *) (** - * Instanciate the current Coq goal with a Micromega formula, a varmap, and a + * Instantiate the current Coq goal with a Micromega formula, a varmap, and a * witness. *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 0209030b64..f038f8a71a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -21,7 +21,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli index 4e7a388aaf..d2f3e756a9 100644 --- a/plugins/micromega/persistent_cache.mli +++ b/plugins/micromega/persistent_cache.mli @@ -17,7 +17,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 6aebc4ca9a..e3a9f6f60f 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -200,7 +200,7 @@ let is_undefined f = | _ -> false;; (* ------------------------------------------------------------------------- *) -(* Operation analagous to "map" for lists. *) +(* Operation analogous to "map" for lists. *) (* ------------------------------------------------------------------------- *) let mapf = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 1777418ef6..bece316c7d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -267,7 +267,7 @@ module PIdeal = Ideal.Make(Poly) open PIdeal (* term to sparse polynomial - varaibles <=np are in the coefficients + variables <=np are in the coefficients *) let term_pol_sparse nvars np t= diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 5db587b9cc..f6ca232c2e 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -357,7 +357,7 @@ let remP v p = moinsP p (multP (coefDom v p) (puisP (x v) (deg v p))) -(* first interger coefficient of p *) +(* first integer coefficient of p *) let rec coef_int_tete p = let v = max_var_pol p in if v>0 @@ -526,7 +526,7 @@ let div_pol_rat p q= (* pseudo division : q = c*x^m+q1 - retruns (r,c,d,s) s.t. c^d*p = s*q + r. + returns (r,c,d,s) s.t. c^d*p = s*q + r. *) let pseudo_div p q x = diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 49d729bd6c..c5f387b248 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -49,7 +49,7 @@ Require Import ssreflect ssrfun. altP (idP my_formula) but circumventing the dependent index capture issue; destructing boolP my_formula generates two subgoals with - assumtions my_formula and ~~ myformula. As + assumptions my_formula and ~~ myformula. As with altP, my_formula must be an application. \unless C, P <-> we can assume property P when a something that holds under condition C (such as C itself). @@ -64,7 +64,7 @@ Require Import ssreflect ssrfun. := forall b : bool, (P -> b) -> b. This is equivalent to ~ (~ P) when P : Prop. implies P Q == wrapper variant type that coerces to P -> Q and - can be used as a P -> Q view unambigously. + can be used as a P -> Q view unambiguously. Useful to avoid spurious insertion of <-> views when Q is a conjunction of foralls, as in Lemma all_and2 below; conversely, avoids confusion in @@ -1003,7 +1003,7 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(** Pseudo-cancellation -- i.e, absorbtion **) +(** Pseudo-cancellation -- i.e, absorption **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. @@ -1245,7 +1245,7 @@ Notation "[ 'pred' x : T | E1 & E2 ]" := (** Coercions for simpl_pred. As simpl_pred T values are used both applicatively and collectively we need simpl_pred to coerce to both pred T _and_ {pred T}. However it is - undesireable to have two distinct constants for what are essentially identical + undesirable to have two distinct constants for what are essentially identical coercion functions, as this confuses the SSReflect keyed matching algorithm. While the Coq Coercion declarations appear to disallow such Coercion aliasing, it is possible to work around this limitation with a combination of modules @@ -1331,9 +1331,9 @@ Variant mem_pred T := Mem of pred T. Similarly to pred_of_simpl, it will usually not be inserted by type inference, as all mem_pred mp =~= pred_sort ?pT unification problems will be solve by the memPredType instance below; pred_of_mem will however - be used if a mem_pred T is used as a {pred T}, which is desireable as it + be used if a mem_pred T is used as a {pred T}, which is desirable as it will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma - expection a generic collective predicate p : {pred T} and premise x \in P + exception a generic collective predicate p : {pred T} and premise x \in P will display a subgoal x \in A rathere than x \in mem A. Conversely, pred_of_mem will _not_ if it is used id (mem A) is used applicatively or as a pred T; there the simpl_of_mem coercion defined below @@ -1396,7 +1396,7 @@ Notation "[ 'rel' x y 'in' A & B ]" := Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope. Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope. -(** Aliases of pred T that let us tag intances of simpl_pred as applicative +(** Aliases of pred T that let us tag instances of simpl_pred as applicative or collective, via bespoke coercions. This tagging will give control over the simplification behaviour of inE and othe rewriting lemmas below. For this control to work it is crucial that collective_of_simpl _not_ @@ -1428,7 +1428,7 @@ Implicit Types (mp : mem_pred T). - registered_applicative_pred: this user-facing structure is used to declare values of type pred T meant to be used applicatively. The structure parameter merely displays this same value, and is used to avoid - undesireable, visible occurrence of the structure in the right hand side + undesirable, visible occurrence of the structure in the right hand side of rewrite rules such as app_predE. There is a canonical instance of registered_applicative_pred for values of the applicative_of_simpl coercion, which handles the @@ -1454,7 +1454,7 @@ Implicit Types (mp : mem_pred T). has been fixed earlier by the manifest_mem_pred match. In particular the definition of a predicate using the applicative_pred_of_simpl idiom above will not be expanded - this very case is the reason in_applicative uses - a mem_pred telescope in its left hand side. The more straighforward + a mem_pred telescope in its left hand side. The more straightforward ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap)) with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...] rather than ?p := Apred in the example above. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 5e3e8ce5fb..572d72ccd8 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -132,7 +132,7 @@ Delimit Scope ssripat_scope with ssripat. Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer - avoids a spurrious trailing %%GEN_IF. **) + avoids a spurious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. @@ -347,10 +347,10 @@ Register protect_term as plugins.ssreflect.protect_term. (** The ssreflect idiom for a non-keyed pattern: - - unkeyed t wiil match any subterm that unifies with t, regardless of + - unkeyed t will match any subterm that unifies with t, regardless of whether it displays the same head symbol as t. - unkeyed t a b will match any application of a term f unifying with t, - to two arguments unifying with with a and b, repectively, regardless of + to two arguments unifying with with a and b, respectively, regardless of apparent head symbols. - unkeyed x where x is a variable will match any subterm with the same type as x (when x would raise the 'indeterminate pattern' error). **) @@ -380,7 +380,7 @@ Notation "=^~ r" := (ssr_converse r) : form_scope. locked_with k t is equal but not convertible to t, much like locked t, but supports explicit tagging with a value k : unit. This is used to mitigate a flaw in the term comparison heuristic of the Coq kernel, - which treats all terms of the form locked t as equal and conpares their + which treats all terms of the form locked t as equal and compares their arguments recursively, leading to an exponential blowup of comparison. For this reason locked_with should be used rather than locked when defining ADT operations. The unlock tactic does not support locked_with @@ -523,7 +523,7 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. elim/abstract_context: (pattern) => G defG. vm_compute; rewrite {}defG {G}. Note that vm_cast are not stored in the proof term - for reductions occuring in the context, hence + for reductions occurring in the context, hence set here := pattern; vm_compute in (value of here) blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : @@ -637,7 +637,7 @@ Ltac over := later complain that it cannot erase _top_assumption_ after having abstracted the viewed assumption. Making x and y maximal implicits would avoid this and force the intended @Some_inj nat x y _top_assumption_ - interpretation, but is undesireable as it makes it harder to use Some_inj + interpretation, but is undesirable as it makes it harder to use Some_inj with the many SSReflect and MathComp lemmas that have an injectivity premise. Specifying {T : nonPropType} solves this more elegantly, as then (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop. @@ -655,13 +655,13 @@ Module NonPropType. maybeProp T to tt and use the test_negative instance and set ?r to false. - call_of c r sets up a call to test_of on condition c with expected result r. It has a default instance for its 'callee' projection to Type, which - sets c := maybeProj T and r := false whe unifying with a type T. + sets c := maybeProj T and r := false when unifying with a type T. - type is a telescope on call_of c r, which checks that unifying test_of ?r1 with c indeed sets ?r1 := r; the type structure bundles the 'test' instance and its 'result' value along with its call_of c r projection. The default instance essentially provides eta-expansion for 'type'. This is only essential for the first 'result' projection to bool; using the instance - for other projection merely avoids spurrious delta expansions that would + for other projection merely avoids spurious delta expansions that would spoil the notProp T notation. In detail, unifying T =~= ?S with ?S : nonPropType, i.e., (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 675e4d2457..dbc9bb24c5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -96,7 +96,7 @@ let subgoals_tys sigma (relctx, concl) = * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None - * 4. build the tactic handle intructions and clears as required in ipats and + * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) let get_eq_type gl = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 93c0d5c236..59fc69f100 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -128,7 +128,7 @@ let newssrcongrtac arg ist gl = x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in - (* here thw two cases: simple equality or arrow *) + (* here the two cases: simple equality or arrow *) let equality, _, eq_args, gl' = let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in @@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) -(* such a generic Leibnitz equation -- short of inspecting the type *) +(* such a generic Leibniz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match Constr.kind c with diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 25975c84e8..6d1d858648 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -143,7 +143,7 @@ val mk_tpattern : type find_P = env -> constr -> int -> k:subst -> constr -(** [conclude ()] asserts that all mentioned ocurrences have been visited. +(** [conclude ()] asserts that all mentioned occurrences have been visited. @return the instance of the pattern, the evarmap after the pattern instantiation, the proof term and the ssrdit stored in the tpattern @raise UserEerror if too many occurrences were specified *) diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 1701bf4365..40946a8d56 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -48,7 +48,7 @@ Ltac2 @ external make : kind -> constr := "ltac2" "constr_make". Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check". (** Checks that a constr generated by unsafe means is indeed safe in the current environment, and returns it, or the error otherwise. Panics if - not focussed. *) + not focused. *) Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl". (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with @@ -68,6 +68,6 @@ Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "const End Unsafe. Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context". -(** On a focussed goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a - focussed goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is +(** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a + focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is the proof built by the tactic. *) diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v index 8d1fb0cd8a..5e8eef526e 100644 --- a/user-contrib/Ltac2/Pattern.v +++ b/user-contrib/Ltac2/Pattern.v @@ -25,7 +25,7 @@ Ltac2 @ external empty_context : unit -> context := Ltac2 @ external matches : t -> constr -> (ident * constr) list := "ltac2" "pattern_matches". (** If the term matches the pattern, returns the bound variables. If it doesn't, - fail with [Match_failure]. Panics if not focussed. *) + fail with [Match_failure]. Panics if not focused. *) Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) := "ltac2" "pattern_matches_subterm". |