aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/tactics.rst18
-rw-r--r--doc/tools/Translator.tex2
-rw-r--r--ide/nanoPG.ml2
-rw-r--r--kernel/clambda.ml2
-rw-r--r--lib/future.ml6
-rw-r--r--lib/future.mli4
-rw-r--r--plugins/funind/functional_principles_proofs.ml26
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/omega/PreOmega.v4
-rw-r--r--plugins/omega/omega.ml2
-rw-r--r--plugins/romega/ReflOmegaCore.v2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
-rw-r--r--stm/stm.ml8
-rw-r--r--test-suite/bugs/closed/4132.v2
-rw-r--r--test-suite/success/univers.v2
-rw-r--r--tools/coq_makefile.ml2
-rw-r--r--tools/coqdoc/output.ml2
-rw-r--r--tools/coqworkmgr.ml2
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/obligations.ml2
20 files changed, 47 insertions, 47 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 9b4d724e0..d1a685307 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -113,15 +113,15 @@ Occurrence sets and occurrence clauses
An occurrence clause is a modifier to some tactics that obeys the
following syntax:
-.. _tactic_occurence_grammar:
+.. _tactic_occurrence_grammar:
.. productionlist:: `sentence`
- occurence_clause : in `goal_occurences`
- goal_occurences : [ident [`at_occurences`], ... , ident [`at_occurences`] [|- [* [`at_occurences`]]]]
- :| * |- [* [`at_occurences`]]
- :| *
+ occurrence_clause : in `goal_occurrences`
+ goal_occurrences : [ident [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]]
+ :| * |- [* [`at_occurrences`]]
+ :| *
at_occurrences : at `occurrences`
- occurences : [-] `num` ... `num`
+ occurrences : [-] `num` ... `num`
The role of an occurrence clause is to select a set of occurrences of a term in
a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that
@@ -1002,7 +1002,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
This notation allows specifying which occurrences of :n:`@term` have to be
substituted in the context. The :n:`in @goal_occurrences` clause is an
occurrence clause whose syntax and behavior are described in
- :ref:`goal occurences <occurencessets>`.
+ :ref:`goal occurrences <occurencessets>`.
.. tacv:: set (@ident {+ @binder} := @term )
@@ -1483,7 +1483,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
This syntax is used for selecting which occurrences of :n:`@term` the case
analysis has to be done on. The :n:`in @goal_occurrences` clause is an
occurrence clause whose syntax and behavior is described in
- :ref:`occurences sets <occurencessets>`.
+ :ref:`occurrences sets <occurencessets>`.
.. tacv:: destruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
.. tacv:: edestruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
@@ -1631,7 +1631,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
This syntax is used for selecting which occurrences of :n:`@term` the
induction has to be carried on. The :n:`in @goal_occurrences` clause is an
occurrence clause whose syntax and behavior is described in
- :ref:`occurences sets <occurencessets>`. If variables or hypotheses not
+ :ref:`occurrences sets <occurencessets>`. If variables or hypotheses not
mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`,
those are generalized as well in the statement to prove.
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 3ee65d6f2..d8ac640f2 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -490,7 +490,7 @@ to be applied are separated by a {\tt =>}.
to turn implicit only the arguments that are {\em strictly} implicit
(or rigid), i.e. that remains inferable whatever the other arguments
are. For instance {\tt x} inferable from {\tt P x} is not strictly
-inferable since it can disappears if {\tt P} is instanciated by a term
+inferable since it can disappears if {\tt P} is instantiated by a term
which erases {\tt x}.
\begin{transbox}
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 2be5dce42..002722ace 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -189,7 +189,7 @@ let emacs = insert emacs "Emacs" [] [
run "Edit" "Cut";
{ s with kill = Some(txt,false); sel = false }
else s));
- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
+ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ ->
let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
let k =
if i#ends_line then begin
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index f1b6f3dff..32a4bd650 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -763,7 +763,7 @@ and lambda_of_app env f args =
and such, which can't be done at this time.
for instance, for int31: if one of the digit is
not closed, it's not impossible that the number
- gets fully instanciated at run-time, thus to ensure
+ gets fully instantiated at run-time, thus to ensure
uniqueness of the representation in the vm
it is necessary to try and build a caml integer
during the execution *)
diff --git a/lib/future.ml b/lib/future.ml
index 7a5b6f699..b372bedc5 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -49,7 +49,7 @@ end
module UUIDMap = Map.Make(UUID)
module UUIDSet = Set.Make(UUID)
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
(* Val is not necessarily a final state, so the
computation restarts from the state stocked into Val *)
@@ -103,7 +103,7 @@ let from_here ?(fix_exn=id) v = create fix_exn (Val v)
let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
let create_delegate ?(blocking=true) ~name fix_exn =
- let assignement signal ck = fun v ->
+ let assignment signal ck = fun v ->
let _, _, fix_exn, c = get ck in
assert (match !c with Delegated _ -> true | _ -> false);
begin match v with
@@ -118,7 +118,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
(fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
(fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
let ck = create ~name fix_exn (Delegated wait) in
- ck, assignement signal ck
+ ck, assignment signal ck
(* TODO: get rid of try/catch to be stackless *)
let rec compute ck : 'a value =
diff --git a/lib/future.mli b/lib/future.mli
index d9e8c87b2..55f05518b 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -70,10 +70,10 @@ val fix_exn_of : 'a computation -> fix_exn
(* Run remotely, returns the function to assign.
If not blocking (the default) it raises NotReady if forced before the
delegate assigns it. *)
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
val create_delegate :
?blocking:bool -> name:string ->
- fix_exn -> 'a computation * ('a assignement -> unit)
+ fix_exn -> 'a computation * ('a assignment -> unit)
(* Given a computation that is_exn, replace it by another one *)
val replace : 'a computation -> 'a computation -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 533694864..3154154ff 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -638,11 +638,11 @@ let my_orelse tac1 tac2 g =
(* observe (str "using snd tac since : " ++ CErrors.print e); *)
tac2 g
-let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
+let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
let args = Array.of_list (List.map mkVar args_id) in
- let instanciate_one_hyp hid =
+ let instantiate_one_hyp hid =
my_orelse
- ( (* we instanciate the hyp if possible *)
+ ( (* we instantiate the hyp if possible *)
fun g ->
let prov_hid = pf_get_new_id hid g in
let c = mkApp(mkVar hid,args) in
@@ -678,7 +678,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
tclTHENLIST
[
tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
- tclMAP instanciate_one_hyp hyps;
+ tclMAP instantiate_one_hyp hyps;
(fun g ->
let all_g_hyps_id =
List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
@@ -722,11 +722,11 @@ let build_proof
tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
(fun g' ->
let g'_nb_prod = nb_prod (project g') (pf_concl g') in
- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in
observe_tac "treat_new_case"
(treat_new_case
ptes_infos
- nb_instanciate_partial
+ nb_instantiate_partial
(build_proof do_finalize)
t
dyn_infos)
@@ -760,7 +760,7 @@ let build_proof
nb_rec_hyps = List.length new_hyps
}
in
-(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
+(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
(* build_proof do_finalize new_infos g' *)
) g
| _ ->
@@ -1120,7 +1120,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
(full_params, (* real params *)
princ_params, (* the params of the principle which are not params of the function *)
- substl (* function instanciated with real params *)
+ substl (* function instantiated with real params *)
(List.map var_of_decl full_params)
f_body
)
@@ -1130,7 +1130,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let f_body = compose_lam f_ctxt_other f_body in
(princ_info.params, (* real params *)
[],(* all params are full params *)
- substl (* function instanciated with real params *)
+ substl (* function instantiated with real params *)
(List.map var_of_decl princ_info.params)
f_body
)
@@ -1321,7 +1321,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
(* ); *)
- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac
+ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id))
]
@@ -1371,7 +1371,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
do_prove
dyn_infos
in
- instanciate_hyps_with_args prove_tac
+ instantiate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id)
]
@@ -1728,8 +1728,8 @@ let prove_principle_for_gen
ptes_info
(body_info rec_hyps)
in
- (* observe_tac "instanciate_hyps_with_args" *)
- (instanciate_hyps_with_args
+ (* observe_tac "instantiate_hyps_with_args" *)
+ (instantiate_hyps_with_args
make_proof
(List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
(List.rev args_ids)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7298342e1..118bcde8b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1318,7 +1318,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| None ->
try add_suffix current_proof_name "_subproof"
with e when CErrors.noncritical e ->
- anomaly (Pp.str "open_new_goal with an unamed theorem.")
+ anomaly (Pp.str "open_new_goal with an unnamed theorem.")
in
let na = next_global_ident_away name Id.Set.empty in
if Termops.occur_existential sigma gls_type then
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 59fd9b801..bc31cb98e 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -181,7 +181,7 @@ Ltac zify_nat_op :=
let t := eval compute in (Z.of_nat (S a)) in
change (Z.of_nat (S a)) with t in H
| _ => rewrite (Nat2Z.inj_succ a) in H
- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
hide [Z.of_nat (S a)] in this one hypothesis *)
change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
end
@@ -192,7 +192,7 @@ Ltac zify_nat_op :=
let t := eval compute in (Z.of_nat (S a)) in
change (Z.of_nat (S a)) with t
| _ => rewrite (Nat2Z.inj_succ a)
- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
hide [Z.of_nat (S a)] in the goal *)
change (Z.of_nat (S a)) with (Z_of_nat' (S a))
end
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 2510c1693..7bca7c709 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -178,7 +178,7 @@ let rec display_action print_var = function
| DIVIDE_AND_APPROX (e1,e2,k,d) ->
Printf.printf
"Inequation E%d is divided by %s and the constant coefficient is \
- rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
+ rounded by subtracting %s.\n" e1.id (sbi k) (sbi d)
| NOT_EXACT_DIVIDE (e,k) ->
Printf.printf
"Constant in equation E%d is not divisible by the pgcd \
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 51b99b993..f4ac202f2 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1866,7 +1866,7 @@ Qed.
End IntOmega.
-(** For now, the above modular construction is instanciated on Z,
+(** For now, the above modular construction is instantiated on Z,
in order to retrieve the initial ROmega. *)
Module ZOmega := IntOmega(Z_as_Int).
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 05eda14e9..13ff817df 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -853,7 +853,7 @@ let rec uniquize = function
let p' = mkApp (pf, pa) in
if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++
- str(String.plural !nocc " occurence") ++ match upats_origin with
+ str(String.plural !nocc " occurrence") ++ match upats_origin with
| None -> str" of" ++ spc() ++ pr_constr_pat p'
| Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++
ws 4 ++ pr_constr_pat p' ++ fnl () ++
diff --git a/stm/stm.ml b/stm/stm.ml
index e15b6048b..6827ec03f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1334,7 +1334,7 @@ module rec ProofTask : sig
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1373,7 +1373,7 @@ end = struct (* {{{ *)
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1813,7 +1813,7 @@ and TacTask : sig
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
- t_assign : output Future.assignement -> unit;
+ t_assign : output Future.assignment -> unit;
t_ast : int * aast;
t_goal : Goal.goal;
t_kill : unit -> unit;
@@ -1830,7 +1830,7 @@ end = struct (* {{{ *)
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
- t_assign : output Future.assignement -> unit;
+ t_assign : output Future.assignment -> unit;
t_ast : int * aast;
t_goal : Goal.goal;
t_kill : unit -> unit;
diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v
index 806ffb771..67ecc3087 100644
--- a/test-suite/bugs/closed/4132.v
+++ b/test-suite/bugs/closed/4132.v
@@ -26,6 +26,6 @@ Qed.
Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
omega. (* Pierre L: according to a comment of bug report #4132,
- this might have triggered "Failure(occurence 2)" in the past,
+ this might have triggered "Failure(occurrence 2)" in the past,
but I never managed to reproduce that. *)
Qed.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 286340459..28426b570 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,7 +60,7 @@ Qed.
Record U : Type := { A:=Type; a:A }.
-(** Check assignement of sorts to inductives and records. *)
+(** Check assignment of sorts to inductives and records. *)
Variable sh : list nat.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ad489da82..33ced97ed 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,7 +48,7 @@ let usage_common () =
\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
\n as a dependencies of an already defined target \"foo\".\
\n[-I dir]: look for Objective Caml dependencies in \"dir\"\
-\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
+\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\
\n starting from \"physicalpath\". The logical path associated to the\
\n physical path is \"logicalpath\".\
\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 05bc6aea9..750698a1c 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -76,7 +76,7 @@ let is_tactic =
[ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
"elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor";
"econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
- "info"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
+ "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto";
"quote"; "eexact"; "autorewrite";
"destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
"f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index 68aadcfcc..bfea141bb 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -169,7 +169,7 @@ let main () =
"-j",Arg.Set_int max_tokens, "max number of concurrent jobs";
"-d",Arg.Set debug, "do not detach (debug)"] in
let usage =
- "Prints on stdout an env variable assignement to be picked up by coq\n"^
+ "Prints on stdout an env variable assignment to be picked up by coq\n"^
"instances in order to limit the maximum number of concurrent workers.\n"^
"The default value is 2.\n"^
"Usage:" in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 102a98f04..ad21a6d9e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -255,7 +255,7 @@ let do_program_recursive local poly fixkind fixl ntns =
interp_recursive ~cofix ~program_mode:true fixl ntns
in
(* Program-specific code *)
- (* Get the interesting evars, those that were not instanciated *)
+ (* Get the interesting evars, those that were not instantiated *)
let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
(* Solve remaining evars *)
let evd = nf_evar_map_undefined evd in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 14d764232..abea7ff9d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -342,7 +342,7 @@ open Goptions
let _ =
declare_bool_option
{ optdepr = false;
- optname = "Hidding of Program obligations";
+ optname = "Hiding of Program obligations";
optkey = ["Hide";"Obligations"];
optread = get_hide_obligations;
optwrite = set_hide_obligations; }
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-23 09:54:24 +0000