diff options
| author | Pierre-Marie Pédrot | 2014-05-20 19:56:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-20 20:03:00 +0200 |
| commit | bf18afeefa06e972c6cb98fa8a81ec7172fdde7f (patch) | |
| tree | 78b737079c541e425c160506d9b80577f389f091 /printing/pptactic.ml | |
| parent | b6fea49600a5b6089eeeea877f06f0e197a0eafb (diff) | |
Moving (e)transitivity out of the AST.
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) -> |