From 73cdb000ec07ec484557839c4b94fcf779df2f06 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 May 2016 00:16:09 +0200
Subject: Put the "clear" tactic into the monad.

---
 printing/printer.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index a16a92d0a5..401f5f99e9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -711,9 +711,6 @@ let pr_prim_rule = function
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
 
-  | Thin ids ->
-      (str"clear "  ++ pr_sequence pr_id ids)
-
   | Move (id1,id2) ->
       (str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
 
-- 
cgit v1.2.3