From 7d436786e79b79643999cddff70f5fbf3b4c3ad9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 22 Feb 2019 14:03:27 +0100
Subject: Remove unused Retroknowledge.Register_inline

This operation is done directly in Safe_typing.register_inline and has
nothing to do with retroknowledge afaict.
---
 kernel/retroknowledge.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 18fafdb6d3..e1c4cec5b5 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -38,4 +38,3 @@ let empty = {
 type action =
   | Register_ind of CPrimitives.prim_ind * inductive
   | Register_type of CPrimitives.prim_type * Constant.t
-  | Register_inline of Constant.t
-- 
cgit v1.2.3