aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/logic.mli')
-rw-r--r--proofs/logic.mli5
1 files changed, 0 insertions, 5 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0a641e975..561c26a7f 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -60,8 +60,3 @@ type refiner_error =
exception RefinerError of refiner_error
val catchable_exception : exn -> bool
-
-
-(*s Pretty-printer. *)
-
-val pr_prim_rule : prim_rule -> Pp.std_ppcmds