aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/tactics.rst8
-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/ssrmatching/ssrmatching.ml2
-rw-r--r--stm/stm.ml8
-rw-r--r--test-suite/bugs/closed/bug_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
19 files changed, 41 insertions, 41 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 794804a1f6..26f4ec6242 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -103,7 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
.. exn:: Not the right number of missing arguments.
-.. _occurencessets:
+.. _occurrencessets:
Occurrence sets and occurrence clauses
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1024,7 +1024,7 @@ Managing the local context
This notation allows specifying which occurrences of :token:`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 <occurrencessets>`.
.. tacv:: set (@ident @binders := @term) {? in @goal_occurrences }
@@ -1509,7 +1509,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
This syntax is used for selecting which occurrences of :token:`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>`.
+ in :ref:`occurrences sets <occurrencessets>`.
.. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
@@ -1659,7 +1659,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 <occurrencessets>`. 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 3ee65d6f22..d8ac640f2a 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 2be5dce426..002722ace9 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 c21ce22421..1e4dbfd418 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -764,7 +764,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 7a5b6f699b..b372bedc5d 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 d9e8c87b21..55f05518b0 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 b12364d04a..98d68d3db7 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 89dfb58017..9fa333c629 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,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 094adfda7a..94a3d40441 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -183,7 +183,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
@@ -194,7 +194,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 2510c16934..7bca7c7099 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/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index aadb4fe5f6..4a63dd4708 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -856,7 +856,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 b7ba163309..19915b1600 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1364,7 +1364,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 }
@@ -1403,7 +1403,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 }
@@ -1843,7 +1843,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;
@@ -1860,7 +1860,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/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 806ffb771f..67ecc3087f 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_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 2863404590..28426b5700 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 c3bdf656d1..0e56cc3c0f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -59,7 +59,7 @@ let usage_coq_makefile () =
\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 8ec8927abd..606d954672 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -71,7 +71,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 68aadcfccf..bfea141bb3 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 ab898644c0..cea8af3f05 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -244,7 +244,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 bdf74bf63d..5352cf5f8c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -348,7 +348,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.25.1) at 2026-01-31 15:29:44 +0000