diff options
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 0ea8b4048c..a5b07c4770 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -790,8 +790,6 @@ and pr_atom1 = function (* Equivalence relations *) | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls - | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c - | TacTransitivity None -> str "etransitivity" (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> |