diff options
| author | Emilio Jesus Gallego Arias | 2018-10-15 15:31:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-15 15:31:27 +0200 |
| commit | fca9ec68937e047d3895d05e57de462387737796 (patch) | |
| tree | f6fc75f7e6be6b60ceafff3afa9d7e13b3219571 /tools/coqdoc | |
| parent | b7dae2c97cce2a298bfbbd6f3a72a02e092ebe9e (diff) | |
| parent | 06cd051d140a183229cd43f0bbae152d6ad8d6ca (diff) | |
Merge PR #8589: Correct some spelling errors (continued)
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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"; |