From 91df402729f70144a4e4d198c4384dc515920e59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 15:42:43 +0200
Subject: Moving the last bits of abtraction-breaking code out of the kernel.

---
 API/API.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 029f458cc7..9f7a6ded81 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4669,8 +4669,6 @@ sig
   val constant_has_body : Declarations.constant_body -> bool
   val is_opaque : Declarations.constant_body -> bool
   val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
-  val body_of_constant :
-    Opaqueproof.opaquetab -> Declarations.constant_body -> Term.constr option
 end
 
 module Constr :
-- 
cgit v1.2.3