From 234f5479773d43a48e67c5c0ea361445c7fb6782 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sun, 22 Jul 2018 18:19:26 -0400 Subject: Correct some spelling errors Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`. --- plugins/omega/PreOmega.v | 4 ++-- plugins/omega/omega.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/omega') 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 \ -- cgit v1.2.3