diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_subst.ml | 3 | ||||
| -rw-r--r-- | kernel/primred.ml | 4 | ||||
| -rw-r--r-- | kernel/retroknowledge.ml | 1 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 1 |
4 files changed, 0 insertions, 9 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? 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 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 diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 1554fe88da..09e8140308 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -25,4 +25,3 @@ val empty : retroknowledge type action = | Register_ind of CPrimitives.prim_ind * inductive | Register_type of CPrimitives.prim_type * Constant.t - | Register_inline of Constant.t |