aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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
6 files changed, 19 insertions, 19 deletions
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 () ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 18:31:09 +0000