diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 26 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/omega/PreOmega.v | 4 | ||||
-rw-r--r-- | plugins/omega/omega.ml | 2 | ||||
-rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 | ||||
-rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 |
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 () ++ |