From 466c25ea43149deedf50e0105a6d1e69db91c8fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Sep 2014 17:58:12 +0200
Subject: Removing the old implementation of clear_body.

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

(limited to 'proofs/proof_type.ml')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 7297706e1d..76459a59ac 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -35,7 +35,6 @@ type prim_rule =
   | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
   | Thin of Id.t list
-  | ThinBody of Id.t list
   | Move of bool * Id.t * Id.t move_location
   | Rename of Id.t * Id.t
 
-- 
cgit v1.2.3