diff options
98 files changed, 122 insertions, 122 deletions
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 55b46c616c..052014824f 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -131,7 +131,7 @@ mingwinCygwin: Install coq in the default Cygwin mingw sysroot folder. Todo: The coq share folder should be configured to e.g. /share/coq. As is, coqc scans the complete share folder, which slows it down 5x for short files. -absoloute: Install coq in the absolute path given with -destcoq. +absolute: Install coq in the absolute path given with -destcoq. The resulting Coq will not be relocatable. That is the root folder must not be renamed/moved. @@ -299,7 +299,7 @@ The version of Coq to download and compile. Possible values: 8.4pl6, 8.5pl2, 8.5pl3, 8.6 (download from https://coq.inria.fr/distrib/V$COQ_VERSION/files/coq-<version>.tar.gz) Others versions might work, but are untested. - 8.4 is only tested in mode=absoloute + 8.4 is only tested in mode=absolute git-v8.6, git-trunk (download from https://github.com/coq/coq/archive/<version without git->.zip) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 5e3a3c3347..88fcb71e77 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -11,10 +11,10 @@ open Names open Univ open Constr -(*******************************************) +(********************************************) (* Initialization of the abstract machine ***) -(* Necessary for [relaccu_tbl] *) -(*******************************************) +(* Necessary for [relaccu_tbl] *) +(********************************************) external init_vm : unit -> unit = "init_coq_vm" diff --git a/lib/pp.mli b/lib/pp.mli index 8b3a07d4b2..bc20a66824 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 against 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/util.ml b/lib/util.ml index 38d73d3453..6e8b8de5dc 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -14,7 +14,7 @@ let on_fst f (a,b) = (f a,b) let on_snd f (a,b) = (a,f b) let map_pair f (a,b) = (f a,f b) -(* Mapping under pairs *) +(* Mapping under triplets *) let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) diff --git a/lib/util.mli b/lib/util.mli index 1eb60f509a..9a00ee3440 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,7 +17,7 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Mapping under triple *) +(** Mapping under triplets *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 59fc69f100..538d0c4e9a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -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 Leibniz 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/pretyping/cases.ml b/pretyping/cases.ml index d7a6c4c832..fadf290d44 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -824,7 +824,7 @@ let push_alias_eqn sigma alias eqn = (**********************************************************************) (* Functions to deal with elimination predicate *) -(* Infering the predicate *) +(* Inferring the predicate *) (* The problem to solve is the following: @@ -1455,7 +1455,7 @@ let compile ~program_mode sigma pb = (* Building the sub-problem when all patterns are variables. Case - where [current] is an intially pushed term. *) + where [current] is an initially pushed term. *) and shift_problem ((current,t),_,na) sigma pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in @@ -1542,7 +1542,7 @@ let compile ~program_mode sigma pb = mat = List.map drop_alias_eqn pb.mat } in compile sigma pb in - (* If the "match" was orginally over a variable, as in "match x with + (* If the "match" was originally over a variable, as in "match x with O => true | n => n end", we give preference to non-expansion in the default clause (i.e. "match x with O => true | n => n end" rather than "match x with O => true | S p => S p end"; @@ -2067,7 +2067,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty let p2 = prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in (* Third strategy: we take the type constraint as it is; of course we could *) - (* need something inbetween, abstracting some but not all of the dependencies *) + (* need something in between, abstracting some but not all of the dependencies *) (* the "inversion" strategy deals with that but unification may not be *) (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *) (* work (yet) when a constructor has a type not precise enough for the inversion *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 5ea9b79336..4aa55e4d0d 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -477,7 +477,7 @@ and cbv_stack_value info env = function cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk) | Some v -> cbv_stack_value info env (v,stk) | None -> mkSTACK(PRIMITIVE(op,c,args), stk) - else (* partical application *) + else (* partial application *) (assert (stk = TOP); PRIMITIVE(op,c,appl)) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index eae961714d..04f54a1ad4 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -34,7 +34,7 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error ([unify_delay]) and another that tries to solve such remaining constraints using heuristics ([unify]). *) -(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. +(** These functions allow to pass arbitrary flags to the unifier and can delay constraints. In case the flags are not specified, they default to [default_flags_of TransparentState.full] currently. diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4a941a68b1..0925215b1c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -285,7 +285,7 @@ let noccur_evar env evd evk c = try occur_rec false (0,env) c; true with Occur -> false (***************************************) -(* Managing chains of local definitons *) +(* Managing chains of local definitions *) (***************************************) type alias = @@ -629,7 +629,7 @@ let solve_pattern_eqn env sigma l c = * If a variable and an alias of it are bound to the same instance, we skip * the alias (we just use eq_constr -- instead of conv --, since anyway, * only instances that are variables -- or evars -- are later considered; - * morever, we can bet that similar instances came at some time from + * moreover, we can bet that similar instances came at some time from * the very same substitution. The removal of aliased duplicates is * useful to ensure the uniqueness of a projection. *) @@ -1738,7 +1738,7 @@ let reconsider_unif_constraints unify flags evd = * Returns an optional list of evars that were instantiated, or None * if the problem couldn't be solved. *) -(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) +(* Rq: incomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index cdd36bbba6..bfe3423b11 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -40,7 +40,7 @@ type t val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t -(** Export the underlying environement *) +(** Export the underlying environment *) val env : t -> env diff --git a/pretyping/program.mli b/pretyping/program.mli index a8f5115788..2614e181d6 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -11,7 +11,7 @@ open Names open EConstr -(** A bunch of Coq constants used by Progam *) +(** A bunch of Coq constants used by Program *) val sig_typ : unit -> GlobRef.t val sig_intro : unit -> GlobRef.t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 85e6f51387..2fc9dc2776 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -886,7 +886,7 @@ module CredNative = RedNative(CNativeEntries) (** Generic reduction function with environment Here is where unfolded constant are stored in order to be - eventualy refolded. + eventually refolded. If tactic_mode is true, it uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants @@ -1315,7 +1315,7 @@ let whd_allnolet_stack env = let whd_allnolet env = red_of_state_red (whd_allnolet_state env) -(* 4. Ad-hoc eta reduction, does not subsitute evars *) +(* 4. Ad-hoc eta reduction, does not substitute evars *) let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index ee27aea93f..26801d285e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -62,7 +62,7 @@ type typeclass = { (* Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; - (* The method implementaions as projections. *) + (* The method implementations as projections. *) cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d134c7319f..ad69cb2890 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1219,12 +1219,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * bindings. This may or may not close off all RHSs of * the EVARs. For each EVAR whose RHS is closed off, * we can just apply it, and go on. For each which - * is not closed off, we need to do a mimick step - + * is not closed off, we need to do a mimic step - * in general, we have something like: * * ?X == (c e1 e2 ... ei[Meta(k)] ... en) * - * so we need to do a mimick step, converting ?X + * so we need to do a mimic step, converting ?X * into * * ?X -> (c ?z1 ... ?zn) @@ -1247,7 +1247,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * we can reverse the equation, put it into our metavar * substitution, and keep going. * - * The most efficient mimick possible is, for each + * The most efficient mimic possible is, for each * Meta-var remaining in the term, to declare a * new EVAR of the same type. This is supposedly * determinable from the clausale form context - diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9d3ed40f6c..e495b1af41 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -348,7 +348,7 @@ let tag_var = tag Tag.variable hov 1 (str "`" ++ (surround_impl b' (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) - |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") + |_ -> anomaly (Pp.str "List of generalized binders have always one element.") end | Default b -> match t with diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index f378a5d2dd..abb0d55b39 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -408,7 +408,7 @@ the call to db_goal_map and entering the following: let match_goals ot nt = let nevar_to_oevar = ref StringMap.empty in (* ogname is "" when there is no difference on the current path. - It's set to the old goal's evar name once a rewitten goal is found, + It's set to the old goal's evar name once a rewritten goal is found, at which point the code only searches for the replacing goals (and ot is set to nt). *) let iter2 f l1 l2 = diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c36b0fa337..b022f4596d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -19,7 +19,7 @@ open Reduction open Clenv (* This function put casts around metavariables whose type could not be - * infered by the refiner, that is head of applications, predicates and + * inferred by the refiner, that is head of applications, predicates and * subject of Cases. * Does check that the casted type is closed. Anyway, the refiner would * fail in this case... *) diff --git a/proofs/refine.mli b/proofs/refine.mli index 55dafe521f..b8948a92f3 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -9,7 +9,7 @@ (************************************************************************) (** 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 + is the recommended 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. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bce227dabb..6476e298e6 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -289,7 +289,7 @@ let tclIFTHENTRYELSEMUST tac1 tac2 gl = (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first thats solves the current goal *) +(* Try the first that's solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) diff --git a/stm/stm.ml b/stm/stm.ml index d469994f3f..f680e55a78 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2661,10 +2661,10 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initalization routine *) +(* Main initialization routine *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear at some some point. *) doc_type : stm_doc_type; @@ -3117,7 +3117,7 @@ let ind_len_loc_of_id sid = let compute_indentation ?loc sid = Option.cata (fun loc -> let open Loc in - (* The effective lenght is the lenght on the last line *) + (* The effective length is the length on the last line *) let len = loc.ep - loc.bp in let prev_indent = match ind_len_loc_of_id sid with | None -> 0 diff --git a/stm/stm.mli b/stm/stm.mli index 24c672c973..5e1e9bf5ad 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -50,7 +50,7 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initalization options: +(** Coq initialization options: - [doc_type]: Type of document being created. @@ -63,7 +63,7 @@ type stm_doc_type = *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear at some some point. *) doc_type : stm_doc_type; @@ -86,7 +86,7 @@ type stm_init_options = { (** The type of a STM document *) type doc -(** [init_core] performs some low-level initalization; should go away +(** [init_core] performs some low-level initialization; should go away in future releases. *) val init_core : unit -> unit diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 6dd9a976f9..71d71cd3ca 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -99,7 +99,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* This is important: The [Global] and [Proof Theorem] parts of the goal_kind are not relevant here as build_constant_by_tactic does use the noop terminator; but beware if some day we remove the - redundancy on constrant declaration. This opens up an interesting + redundancy on constraint declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) let goal_kind, suffix = if opaque @@ -164,7 +164,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> - (* We mimick what the kernel does, that is ensuring that no additional + (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 1fae4c3d9d..1170c1acd0 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -30,7 +30,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = if check_scheme kind ind then (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the - apropriate type *) + appropriate type *) let cte, eff = find_scheme kind ind in let sigma, cte = Evd.fresh_constant_instance env sigma cte in let c = mkConstU cte in diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index e75a61d0c6..1a0b7f84cf 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -30,7 +30,7 @@ open Proofview.Notations open Tacmach.New open Tactypes -(* This file containts the implementation of the tactics ``Decide +(* This file contains the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the propositional equality of two objects that belongs to a small inductive datatype --i.e., an inductive set such that all the diff --git a/tactics/equality.mli b/tactics/equality.mli index 6f3e08ea02..7381d5f77b 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -132,7 +132,7 @@ val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic (* Replace term *) (* [replace_term dir_opt c cl] - perfoms replacement of [c] by the first value found in context + performs replacement of [c] by the first value found in context (according to [dir] if given to get the rewrite direction) in the clause [cl] *) val replace_term : bool option -> constr -> clause -> unit Proofview.tactic diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index e1dad9ad20..5ac28cb9e2 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -25,7 +25,7 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration (* I implemented the following functions which test whether a term t - is an inductive but non-recursive type, a general conjuction, a + is an inductive but non-recursive type, a general conjunction, a general disjunction, or a type with no constructors. They are more general than matching with or_term, and_term, etc, diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index b8c3ddb0f0..696b11d9db 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -35,7 +35,7 @@ open Coqlib contained in the arguments of the application *) (** I implemented the following functions which test whether a term [t] - is an inductive but non-recursive type, a general conjuction, a + is an inductive but non-recursive type, a general conjunction, a general disjunction, or a type with no constructors. They are more general than matching with [or_term], [and_term], etc, diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 6efa1ece9c..8cc481e30e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -98,7 +98,7 @@ let get_local_sign sign = in List.fold_right add_local lid nil_sign *) -(* returs the identifier of lid that was the latest declared in sign. +(* returns the identifier of lid that was the latest declared in sign. * (i.e. is the identifier id of lid such that * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) > * for any id'<>id in lid). diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index dcd63fe760..2467671d38 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -481,7 +481,7 @@ module New = struct ) <*> tclUNIT res - (* Try the first thats solves the current goal *) + (* Try the first that's solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) let tclPROGRESS t = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9dafa8bad9..191f00d104 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3019,14 +3019,14 @@ let specialize (c,lbind) ipat = (* We grab names used in product to remember them at re-abstracting phase *) let typ_of_c_hd = pf_get_type_of gl c_hd in let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in - (* accumulator args: arguments to apply to c_hd: all infered + (* accumulator args: arguments to apply to c_hd: all inferred args + re-abstracted rels *) let rec rebuild_lambdas sigma lprd args hd l = match lprd , l with | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> (* nme has not been resolved, let us re-abstract it. Same - name but type updated by instanciation of other args. *) + name but type updated by instantiation of other args. *) let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in let r = Retyping.relevance_of_type env sigma new_typ_of_t in let liftedargs = List.map liftrel args in @@ -4292,7 +4292,7 @@ let induction_tac with_evars params indvars elim = let elimc = contract_letin_in_lam_header sigma elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in let elimclause = Tacmach.New.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in - (* elimclause' is built from elimclause by instanciating all args and params. *) + (* elimclause' is built from elimclause by instantiating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in diff --git a/test-suite/bugs/closed/bug_2137.v b/test-suite/bugs/closed/bug_2137.v index b1f54b1766..981cc94dc1 100644 --- a/test-suite/bugs/closed/bug_2137.v +++ b/test-suite/bugs/closed/bug_2137.v @@ -3,7 +3,7 @@ The fsetdec tactic is sensitive to which way round the arguments to <> are. In the small, self-contained example below, it is able to solve the goal if it knows that "b <> a", but not if it knows that "a <> b". I would expect -it to be able to solve hte goal in either case. +it to be able to solve the goal in either case. I have coq r12238. diff --git a/test-suite/bugs/closed/bug_2603.v b/test-suite/bugs/closed/bug_2603.v index 371bfdc575..64c656a7a6 100644 --- a/test-suite/bugs/closed/bug_2603.v +++ b/test-suite/bugs/closed/bug_2603.v @@ -3,7 +3,7 @@ As noticed by A. Appel in bug #2603, module names and definition names used to be in the same namespace. But conflict with names of constructors (or 2nd mutual inductive...) used to not be checked -enough, leading to stange situations. +enough, leading to strange situations. - In 8.3pl3 we introduced checks that forbid uniformly the following situations. diff --git a/test-suite/bugs/closed/bug_3080.v b/test-suite/bugs/closed/bug_3080.v index 36ab7ff599..06719653fe 100644 --- a/test-suite/bugs/closed/bug_3080.v +++ b/test-suite/bugs/closed/bug_3080.v @@ -15,4 +15,4 @@ Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : function_scope. Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *) -Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *) +Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arguments to [compose] *) diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v index 5162f352df..26731e3292 100644 --- a/test-suite/bugs/closed/bug_4503.v +++ b/test-suite/bugs/closed/bug_4503.v @@ -29,7 +29,7 @@ End ILogic. Set Printing Universes. -(* There is stil a problem if the class is universe polymorphic *) +(* There is still a problem if the class is universe polymorphic *) Section Embed_ILogic_Pre. Polymorphic Universes A T. Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. diff --git a/test-suite/bugs/closed/bug_4720.v b/test-suite/bugs/closed/bug_4720.v index 704331e784..a870792c39 100644 --- a/test-suite/bugs/closed/bug_4720.v +++ b/test-suite/bugs/closed/bug_4720.v @@ -34,7 +34,7 @@ End WithModPriv. identical by the extraction. In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv - were all causing Anomaly or Assert Failure. This shoud be fixed now. + were all causing Anomaly or Assert Failure. This should be fixed now. *) Require Extraction. diff --git a/test-suite/bugs/closed/bug_5123.v b/test-suite/bugs/closed/bug_5123.v index 17231bffcf..a4029aeee0 100644 --- a/test-suite/bugs/closed/bug_5123.v +++ b/test-suite/bugs/closed/bug_5123.v @@ -28,6 +28,6 @@ Goal True. opose (@vect_sigT_eqdec _ _ _ _) as H. Unshelve. all:cycle 3. - eapply existT. (*This does no typeclass resultion, which is correct.*) + eapply existT. (*This does no typeclass resolution, which is correct.*) Focus 5. Abort. diff --git a/test-suite/bugs/closed/bug_5149.v b/test-suite/bugs/closed/bug_5149.v index ae32217057..b56abfe42e 100644 --- a/test-suite/bugs/closed/bug_5149.v +++ b/test-suite/bugs/closed/bug_5149.v @@ -36,7 +36,7 @@ Proof. solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail "too early". Undo. - (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) + (** Implicitly at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ]. solve [eapply interpf_SmartVarVar; subst; eassumption]. Undo. diff --git a/test-suite/bugs/closed/bug_808_2411.v b/test-suite/bugs/closed/bug_808_2411.v index 1169b2036b..9fe4c9d503 100644 --- a/test-suite/bugs/closed/bug_808_2411.v +++ b/test-suite/bugs/closed/bug_808_2411.v @@ -2,7 +2,7 @@ Section test. Variable n:nat. Lemma foo: 0 <= n. Proof. -(* declaring an Axiom during a proof makes it immediatly +(* declaring an Axiom during a proof makes it immediately usable, juste as a full Definition. *) Axiom bar : n = 1. rewrite bar. diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index 0d75d52a31..d2e6794c0b 100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dcc8bd7165..29614c032a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -209,7 +209,7 @@ Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun Check exists_mixed x y '(u,t), x+y=0/\u+t=0. Check exists_mixed x y '(z,t), x+y=0/\z+t=0. -(* Check that intermediary let-in are inserted inbetween instances of +(* Check that intermediary let-in are inserted in between instances of the repeated pattern *) Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 3c427237b4..69ed621877 100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 69fca48e24..ba6bf3bba2 100644 --- a/test-suite/success/Case15.v +++ b/test-suite/success/Case15.v @@ -20,7 +20,7 @@ Definition test (B : Boite) := | boite false (n, m) => n + m end. -(* Check lazyness of compilation ... future work +(* Check laziness of compilation ... future work Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. Check [x] diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 8d9edbd62d..b0398ca056 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -62,7 +62,7 @@ Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option n (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) -(* This exemple extracted from the developement done by Nacira Chabane *) +(* This exemple extracted from the development done by Nacira Chabane *) (* (equipe Paris 6) *) (* -------------------------------------------------------------------- *) diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 2f13b7c225..e96a5f9048 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -175,7 +175,7 @@ End HintCut. (* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) -(* e.g. those tactics when considering a goal with existential varibles *) +(* e.g. those tactics when considering a goal with existential variables *) (* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) (* See this Coq club post for more detail: *) (* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index ee540d7109..1dbeaf3e1f 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -179,7 +179,7 @@ exact Logic.I. Qed. (* Up to September 2014, H0 below was renamed called H1 because of a collision - with the automaticallly generated names for equations. + with the automatically generated names for equations. (example taken from CoLoR) *) Inductive term := Var | Fun : term -> term -> term. diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v index de9b997590..98759264e5 100644 --- a/test-suite/success/Reordering.v +++ b/test-suite/success/Reordering.v @@ -1,7 +1,7 @@ (* Testing the reordering of hypothesis required by pattern, fold and change. *) Goal forall (A:Set) (x:A) (A':=A), True. intros. -fold A' in x. (* suceeds: x is moved after A' *) +fold A' in x. (* succeeds: x is moved after A' *) Undo. pattern A' in x. Undo. diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index fb0adabae9..c566a6db9f 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -34,7 +34,7 @@ Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) Extraction TestCompile testAbis. -(** 2) With signature, we only keep elements mentionned in signature. *) +(** 2) With signature, we only keep elements mentioned in signature. *) Module Type SIG. Parameter u : nat. diff --git a/test-suite/success/if.v b/test-suite/success/if.v index c81d2b9bf1..68d26ac8df 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -1,4 +1,4 @@ -(* The synthesis of the elimination predicate may fail if algebric *) +(* The synthesis of the elimination predicate may fail if algebraic *) (* universes are not cautiously treated *) Check (fun b : bool => if b then Type else nat). diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 7f26181108..8abd4a3cbb 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -76,7 +76,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -(** The equiv is burried inside the setoid, but we can recover it by specifying +(** The equiv is buried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index f6b240bf20..28394b984e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -77,7 +77,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). Require Import Coq.Arith.Arith. -(** The equiv is burried inside the setoid, but we can recover +(** The equiv is buried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) Program Instance eq_setoid A : Setoid A | 10 := diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 8970529103..a12e4a43c2 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -192,7 +192,7 @@ Module Type WSfun (E : DecidableType). (** Equality of maps *) (** Caveat: there are at least three distinct equality predicates on maps. - - The simpliest (and maybe most natural) way is to consider keys up to + - The simplest (and maybe most natural) way is to consider keys up to their equivalence [E.eq], but elements up to Leibniz equality, in the spirit of [eq_key_elt] above. This leads to predicate [Equal]. - Unfortunately, this [Equal] predicate can't be used to describe diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 83bb07ffb6..d977ac05ec 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -240,7 +240,7 @@ the above form: True. Proof. intros. push not in *. - (* note that ~(R->P) remains (since R isnt decidable) *) + (* note that ~(R->P) remains (since R isn't decidable) *) tauto. Qed. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 1a391ed799..d54c8bf42d 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -37,7 +37,7 @@ Notation "~ x" := (not x) : type_scope. Register not as core.not.type. (** Create the "core" hint database, and set its transparent state for - variables and constants explicitely. *) + variables and constants explicitly. *) Create HintDb core. Hint Variables Opaque : core. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index 7e7a1ced58..5952f3a31b 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -331,7 +331,7 @@ Definition iter (n:nat) {A} (f:A->A) (x:A) : A := (** Bitwise operations *) (** We provide here some bitwise operations for unary numbers. - Some might be really naive, they are just there for fullfiling + Some might be really naive, they are just there for fulfilling the same interface as other for natural representations. As soon as binary representations such as NArith are available, it is clearly better to convert to/from them and use their ops. diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index 419a0be49c..e1e0d3db4c 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -70,7 +70,7 @@ Qed. End MemoFunction. (** For a dependent function, the previous solution is - reused thanks to a temporarly hiding of the dependency + reused thanks to a temporary hiding of the dependency in a "container" [memo_val]. *) Section DependentMemoFunction. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index b06384e992..73d7432193 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -385,7 +385,7 @@ End Proof_irrelevance_EM_CC. fragment of [Prop] into [bool], hence weak classical logic, i.e. [forall A, ~A\/~~A], is enough for deriving a weak version of proof-irrelevance. This is enough to derive a contradiction from a - [Set]-bound weak excluded middle wih an impredicative [Set] + [Set]-bound weak excluded middle with an impredicative [Set] universe. *) Section Proof_irrelevance_WEM_CC. diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index f228cbb3bf..3ceff849be 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -240,7 +240,7 @@ the above form: True. Proof. intros. push not in *. - (* note that ~(R->P) remains (since R isnt decidable) *) + (* note that ~(R->P) remains (since R isn't decidable) *) tauto. Qed. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index a3dcca7dfd..838721f499 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -166,7 +166,7 @@ end. *) (** Enumeration of the elements of a tree. This corresponds - to the "samefringe" notion in the litterature. *) + to the "samefringe" notion in the literature. *) #[universes(template)] Inductive enumeration := diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 6a18f59fc4..85139593da 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -659,7 +659,7 @@ End Raw2Sets. (** It is in fact possible to provide an ordering on sets with very little information on them (more or less only the [In] predicate). This generic build of ordering is in fact not - used for the moment, we rather use a simplier version + used for the moment, we rather use a simpler version dedicated to sets-as-sorted-lists, see [MakeListOrdering]. *) diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index be12fffaaf..3e5987127a 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -25,7 +25,7 @@ Module N. Definition t := N. -(** ** Nicer name [N.pos] for contructor [Npos] *) +(** ** Nicer name [N.pos] for constructor [Npos] *) Notation pos := Npos. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index c7e3999691..6809154a33 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -18,7 +18,7 @@ thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your development, this file provides some alternative [Numeral - Notation] commmands that use [Z] as bridge type. To enable these + Notation] commands that use [Z] as bridge type. To enable these commands, just be sure to [Require] this file after other files defining numeral notations. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 4b0bda3d44..a7bc4211ed 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1288,7 +1288,7 @@ Section Int31_Specs. intros; rewrite <- spec_1; apply spec_add. Qed. - (** Substraction *) + (** Subtraction *) Lemma spec_sub_c : forall x y, [-|sub31c x y|] = [|x|] - [|y|]. Proof. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index b9185c9ca0..10f819b005 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -255,7 +255,7 @@ Definition add31carryc (n m : int31) := | _ => C1 npmpone end. -(** * Substraction *) +(** * Subtraction *) (** Subtraction modulo [2^31] *) diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 4aabda77ee..42ea8f76fb 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -324,7 +324,7 @@ Proof. now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l. Qed. -(** Accesing a high enough bit of a number gives its sign *) +(** Accessing a high enough bit of a number gives its sign *) Lemma bits_iff_nonneg : forall a n, log2 (abs a) < n -> (0<=a <-> a.[n] = false). diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 0ab528de80..377c05e279 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -207,7 +207,7 @@ Qed. We had an abs in order to have an always-nonnegative lcm, in the spirit of gcd. Nota: [lcm 0 0] should be 0, which - isn't garantee with the third equation above. + isn't guarantee with the third equation above. *) Definition lcm a b := abs (a*(b/gcd a b)). diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 5f102e853b..b96a2b35af 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -149,7 +149,7 @@ Proof. intros n m H; apply add_le_cases; now nzsimpl. Qed. -(** Substraction *) +(** Subtraction *) (** We can prove the existence of a subtraction of any number by a smaller one *) diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index acebfcf1d2..cace65c61d 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -310,7 +310,7 @@ Qed. End NZOfNatOrd. -(** For basic operations, we can prove correspondance with +(** For basic operations, we can prove correspondence with their counterpart in [nat]. *) Module NZOfNatOps (Import NZ:NZAxiomsSig'). diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 47b74193ed..19a8b4b2b1 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -90,7 +90,7 @@ Qed. = (a / gcd a b) * b = (a*b) / gcd a b - Nota: [lcm 0 0] should be 0, which isn't garantee with the third + Nota: [lcm 0 0] should be 0, which isn't guarantee with the third equation above. *) diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 7f30733559..1c78011941 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -310,7 +310,7 @@ Infix "<?" := ltb (at level 70, no associativity) : positive_scope. (** ** A Square Root function for positive numbers *) -(** We procede by blocks of two digits : if p is written qbb' +(** We proceed by blocks of two digits : if p is written qbb' then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1. For deciding easily in which case we are, we store the remainder (as a mask, since it can be null). diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 5ae933d433..9fe3b967ae 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -31,7 +31,7 @@ Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. Ltac unblock_goal := unfold block in *. -(** Notation for heterogenous equality. *) +(** Notation for heterogeneous equality. *) Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). @@ -88,7 +88,7 @@ Ltac elim_eq_rect := end end. -(** Rewrite using uniqueness of indentity proofs [H = eq_refl]. *) +(** Rewrite using uniqueness of identity proofs [H = eq_refl]. *) Ltac simpl_uip := match goal with @@ -450,7 +450,7 @@ Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by - writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before + writing another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling [induction]. *) Tactic Notation "dependent" "induction" ident(H) := diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index ec283b886e..c41ab905e0 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1352,7 +1352,7 @@ Proof. Qed. (*********************************************************) -(** ** Order and substraction *) +(** ** Order and subtraction *) (*********************************************************) Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 08bc400f0a..142883a525 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -543,7 +543,7 @@ Qed. End Permut_permut. (* begin hide *) -(** For compatibilty *) +(** For compatibility *) Notation permut_right := permut_cons (only parsing). Notation permut_tran := permut_trans (only parsing). (* end hide *) diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index d000b75bf4..e5b2e22dc1 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -208,7 +208,7 @@ Module OrderedTypeFacts (Import O: OrderedType). unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto. Qed. -(* Specialization of resuts about lists modulo. *) +(* Specialization of results about lists modulo. *) Section ForNotations. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 182b781fe1..354c1eb9b0 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -431,7 +431,7 @@ Proof. apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt. Qed. -(** Relation bewteen [compare] and the boolean comparisons *) +(** Relation between [compare] and the boolean comparisons *) Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index ebd8ee8fc2..80925ff058 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -51,7 +51,7 @@ Local Infix "+" := trans_ord. This used to be provided here via a [TotalOrder], but for technical reasons related to extraction, we now ask - for two sperate parts: relations in a [EqLtLe] + properties in + for two separate parts: relations in a [EqLtLe] + properties in [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder] *) diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index 4088843a1b..0b3e9b78f6 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -160,7 +160,7 @@ Qed. (** The p{^ th} element of [fin m] viewed as the p{^ th} element of [fin (n + m)] -Really really ineficient !!! *) +Really really inefficient !!! *) Definition L_R {m} n (p : t m) : t (n + m). Proof. induction n. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a346ab8ccb..43841920e5 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1259,7 +1259,7 @@ Proof. f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed. -(** * [testbit] in terms of comparision. *) +(** * [testbit] in terms of comparison. *) Lemma testbit_mod_pow2 a n i (H : 0 <= n) : testbit (a mod 2 ^ n) i = ((i <? n) && testbit a i)%bool. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 8cb62622db..a9a5f15f2e 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -28,7 +28,7 @@ Module Z. Definition t := Z. -(** ** Nicer names [Z.pos] and [Z.neg] for contructors *) +(** ** Nicer names [Z.pos] and [Z.neg] for constructors *) Notation pos := Zpos. Notation neg := Zneg. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 0b0ed48d51..9cade75f08 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -13,7 +13,7 @@ (** We define a signature for an integer datatype based on [Z]. The goal is to allow a switch after extraction to ocaml's [big_int] or even [int] when finiteness isn't a problem - (typically : when mesuring the height of an AVL tree). + (typically : when measuring the height of an AVL tree). *) Require Import BinInt. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index a619eb90ef..64431a9411 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -105,7 +105,7 @@ Proof. rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed. -(** This can also be said in a simplier way: *) +(** This can also be said in a simpler way: *) Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a. Proof. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 2ec55d1bd0..d37d2bea94 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -171,7 +171,7 @@ DYNOBJ:=.cmxs DYNLIB:=.cmxs endif -# these variables are meant to be overriden if you want to add *extra* flags +# these variables are meant to be overridden if you want to add *extra* flags COQEXTRAFLAGS?= COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 8823206252..c00fb71dba 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -454,7 +454,7 @@ let usage () = eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; - eprintf " -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; + eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index b703af934d..75667ae909 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -762,7 +762,7 @@ module Html = struct (* inference rules *) let inf_rule assumptions (_,_,midnm) conclusions = - (* this first function replaces any occurance of 3 or more spaces + (* this first function replaces any occurrence of 3 or more spaces in a row with " "s. We do this to the assumptions so that people can put multiple rules on a line with nice formatting *) let replace_spaces str = diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli index 00db2ad317..6449cd5b6f 100644 --- a/tools/coqdoc/tokens.mli +++ b/tools/coqdoc/tokens.mli @@ -57,7 +57,7 @@ val translate : string -> string option dictionary, "<>_h" is one word and gets translated *) -(* Warning: do not output anything on output channel inbetween a call +(* Warning: do not output anything on output channel in between a call to [output_tagged_*] and [flush_sublexer]!! *) type out_function = diff --git a/tools/coqwc.mll b/tools/coqwc.mll index f0f138740c..06b4ad5fd3 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -207,7 +207,7 @@ and string = parse | eof { 0 } (*s The following entry [read_header] is used to skip the possible header at - the beggining of files (unless option \texttt{-e} is specified). + the beginning of files (unless option \texttt{-e} is specified). It stops whenever it encounters an empty line or any character outside a comment. In this last case, it correctly resets the lexer position on that character (decreasing [lex_curr_pos] by 1). *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index cbe353004e..f4ae00ed65 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -17,7 +17,7 @@ let set_debug () = let () = Backtrace.record_backtrace true in Flags.debug := true -(* Loading of the ressource file. +(* Loading of the resource file. rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one does not exist. *) diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 0cc22ba31d..852a65f07b 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -17,7 +17,7 @@ type input_buffer = { mutable prompt : Stm.doc -> string; mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) - mutable bols : int list; (** offsets in str of begining of lines *) + mutable bols : int list; (** offsets in str of beginning of lines *) mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c41f16c95b..41bff34bd3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -37,7 +37,7 @@ let vernac_echo ?loc in_chan = let open Loc in Feedback.msg_notice @@ str @@ really_input_string in_chan len ) loc -(* Reenable when we get back to feedback printing *) +(* Re-enable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) (* | _ -> false *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 635751bb24..c37e90650a 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -146,7 +146,7 @@ let do_assumptions ~program_mode kind nl l = l [] else l in - (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) + (* We interpret all declarations in the same evar_map, i.e. as a telescope. *) let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in let r = Retyping.relevance_of_type env sigma t in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 00f19f545c..a428c42e49 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -333,7 +333,7 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | CStructRec na -> na | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na | CMeasureRec (None,_,_) when not structonly -> - user_err Pp.(str "Decreasing argument must be specificed in measure clause.") + user_err Pp.(str "Decreasing argument must be specified in measure clause.") | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 642695bda4..6ac259b1fe 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind = let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the - apropriate type *) + appropriate type *) if Sorts.List.mem InType kelim then ignore (define_individual_scheme dep UserAutomaticRequest None ind) diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 1bb44d0ef1..f5e8b6d12f 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -206,7 +206,7 @@ let try_locate_absolute_library dir = type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { - unix_path : string; (* Filesystem path contaning vo/ml files *) + unix_path : string; (* Filesystem path containing vo/ml files *) coq_path : DP.t; (* Coq prefix for the path *) implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index d393fc35b5..6605daa8d2 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -68,7 +68,7 @@ type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { unix_path : string; - (** Filesystem path contaning vo/ml files *) + (** Filesystem path containing vo/ml files *) coq_path : Names.DirPath.t; (** Coq prefix for the path *) implicit : bool; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 46c4422d17..ad175511b9 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -331,7 +331,7 @@ let default_tactic = ref (Proofview.tclUNIT ()) let get_hide_obligations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Hidding of Program obligations" + ~name:"Hiding of Program obligations" ~key:["Hide";"Obligations"] ~value:false diff --git a/vernac/search.ml b/vernac/search.ml index e41378908f..a5663d65ef 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -28,7 +28,7 @@ type display_function = GlobRef.t -> env -> constr -> unit [SearchAbout ...], etc. to the names of the symbols matching the query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates -without having to parse thorugh the types of all symbols. *) +without having to parse through the types of all symbols. *) type glob_search_about_item = | GlobSearchSubPattern of constr_pattern diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b9d1326ba5..5ae572541e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -622,7 +622,7 @@ let vernac_end_proof ?pstate ?proof = function let vernac_exact_proof ~pstate c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is - called only at the begining of a proof. *) + called only at the beginning of a proof. *) let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom; diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 54e08d0e95..b37e527f47 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -22,7 +22,7 @@ a query like Check. The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof + parsing, execution (global environment, etc...), and proof state. For example, commands that only alter the proof state are considered safe to delegate to a worker. |