aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/interface/paths.ml
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@google.com>2018-07-22 18:19:26 -0400
committerGravatar Benjamin Barenblat <bbaren@google.com>2018-07-22 18:19:26 -0400
commit234f5479773d43a48e67c5c0ea361445c7fb6782 (patch)
tree0609f0aef4769561d3bee2049c5c973f40b20be3 /plugins/interface/paths.ml
parent32415df7e24d4d79a00fae95a5f619980b006c61 (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/interface/paths.ml')
0 files changed, 0 insertions, 0 deletions