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/printer.ml')

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


From 12f4c8ed277fa8368cab2e99f173339a64bcef3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 18:34:21 +0200
Subject: Put the "fix" tactic in the monad.

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

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 401f5f99e9..4c8e806f43 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -685,18 +685,6 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 
-  | FixRule (f,n,[],_) ->
-      (str"fix " ++ pr_id f ++ str"/" ++ int n)
-
-  | FixRule (f,n,others,j) ->
-      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
-      let rec print_mut = function
-	| (f,n,ar)::oth ->
-           pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
-        | [] -> mt () in
-      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
-         str" with " ++ print_mut others)
-
   | Cofix (f,[],_) ->
       (str"cofix " ++ pr_id f)
 
-- 
cgit v1.2.3


From a4bd166bd2119a5290276f0ded44f8186ba1ecee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 21:21:42 +0200
Subject: Put the "cofix" tactic in the monad.

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

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 4c8e806f43..cb075c64fb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -685,16 +685,6 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 
-  | Cofix (f,[],_) ->
-      (str"cofix " ++ pr_id f)
-
-  | Cofix (f,others,j) ->
-      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
-      let rec print_mut = function
-	| (f,ar)::oth ->
-	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
-        | [] -> mt () in
-      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
   | Refine c ->
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
-- 
cgit v1.2.3