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/primred.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'kernel/primred.ml')

diff --git a/kernel/primred.ml b/kernel/primred.ml
index d95d7de7aa..d6d0a6143a 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -44,10 +44,6 @@ let add_retroknowledge env action =
         { retro with retro_cmp = Some r }
     in
     set_retroknowledge env retro
-  | Register_inline(c) ->
-    let (cb,r) = lookup_constant_key c env in
-    let cb = {cb with Declarations.const_inline_code = true} in
-    add_constant_key c cb !(fst r) env
 
 let get_int_type env =
   match env.retroknowledge.retro_int63 with
-- 
cgit v1.2.3