diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
| commit | 234f5479773d43a48e67c5c0ea361445c7fb6782 (patch) | |
| tree | 0609f0aef4769561d3bee2049c5c973f40b20be3 /plugins/romega | |
| parent | 32415df7e24d4d79a00fae95a5f619980b006c61 (diff) | |
Correct some spelling errorsmaster
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/romega')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |