diff options
| author | Gaëtan Gilbert | 2019-02-22 14:03:27 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-11 13:36:03 +0100 |
| commit | 7d436786e79b79643999cddff70f5fbf3b4c3ad9 (patch) | |
| tree | f0e3f3be303902f178c1ded6294829d8dd06abfc /kernel/mod_subst.ml | |
| parent | 74534f84a782f5de740c52cb97b3ca3a02eb6aa2 (diff) | |
Remove unused Retroknowledge.Register_inline
This operation is done directly in Safe_typing.register_inline and has
nothing to do with retroknowledge afaict.
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 3 |
1 files changed, 0 insertions, 3 deletions
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? |