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 /tools | |
| 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 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 | ||||
| -rw-r--r-- | tools/coqworkmgr.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c3bdf656d1..0e56cc3c0f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -59,7 +59,7 @@ let usage_coq_makefile () = \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ \n as a dependencies of an already defined target \"foo\".\ \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ -\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ +\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ \n starting from \"physicalpath\". The logical path associated to the\ \n physical path is \"logicalpath\".\ \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 8ec8927abd..606d954672 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -71,7 +71,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; + "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index 68aadcfccf..bfea141bb3 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -169,7 +169,7 @@ let main () = "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; "-d",Arg.Set debug, "do not detach (debug)"] in let usage = - "Prints on stdout an env variable assignement to be picked up by coq\n"^ + "Prints on stdout an env variable assignment to be picked up by coq\n"^ "instances in order to limit the maximum number of concurrent workers.\n"^ "The default value is 2.\n"^ "Usage:" in |