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

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index cd675653cb..9397772415 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -339,9 +339,6 @@ let subst_retro_action subst action =
   | Register_type(prim,c) ->
     let c' = subst_constant subst c in
     if c == c' then action else Register_type(prim, c')
-  | Register_inline(c) ->
-    let c' = subst_constant subst c in
-    if c == c' then action else Register_inline(c')
 
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
-- 
cgit v1.2.3