diff options
| author | Benjamin Barenblat | 2018-07-22 18:19:26 -0400 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-15 13:28:52 +0200 |
| commit | 06cd051d140a183229cd43f0bbae152d6ad8d6ca (patch) | |
| tree | 6528aa85924d1cfdb965b81a15b4ec93189554fa /plugins/omega/PreOmega.v | |
| parent | ecf999c8f8a677508d2856c3c8a7cacfa5da3839 (diff) | |
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`.
Diffstat (limited to 'plugins/omega/PreOmega.v')
| -rw-r--r-- | plugins/omega/PreOmega.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 |