diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-22 13:45:03 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-07-17 14:15:59 +0200 |
| commit | 8c43e795c772090b336c0f170a6e5dcab196125d (patch) | |
| tree | 98508f7e342142dd017da56872f74df73e6fce58 /tools | |
| parent | b799252775563b4f46f5ea39cbfc469759e7a296 (diff) | |
Remove fourier plugin
As stated in the manual, the fourier tactic is subsumed by lra.
Diffstat (limited to 'tools')
| -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 c640167ac..05bc6aea9 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -76,7 +76,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"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; + "info"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "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"; |