diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f4007e25e1..689ac6e4eb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -935,10 +935,6 @@ module Make ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h ) - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> hov 1 ( |