diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 10:54:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 10:55:38 +0100 |
| commit | bda8b2e8f90235ca875422f211cb781068b20b3c (patch) | |
| tree | 223ea774824958259dce4289c5ecbee984bc6afc /printing/pptactic.ml | |
| parent | 48327426b59144f1a7181092068077c5a6df7c60 (diff) | |
Moving the "cofix" tactic to TACTIC EXTEND.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fe0be9b25..05c3b3bf4 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -832,8 +832,6 @@ module Make hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) - | TacCofix ido -> - hov 1 (primitive "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> hov 1 ( primitive "cofix" ++ spc () ++ pr_id id ++ spc() |