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.

---
 proofs/proof_type.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs/proof_type.mli')

diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b4c9dae2a3..48ad50c7a0 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -22,7 +22,6 @@ type prim_rule =
   | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Thin of Id.t list
   | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
-- 
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.

---
 proofs/proof_type.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs/proof_type.mli')

diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 48ad50c7a0..ea3b5242da 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -19,7 +19,6 @@ open Misctypes
 
 type prim_rule =
   | Cut of bool * bool * Id.t * types
-  | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
   | Move of Id.t * Id.t move_location
-- 
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.

---
 proofs/proof_type.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs/proof_type.mli')

diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ea3b5242da..ef0d52b62d 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -19,7 +19,6 @@ open Misctypes
 
 type prim_rule =
   | Cut of bool * bool * Id.t * types
-  | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
   | Move of Id.t * Id.t move_location
 
-- 
cgit v1.2.3