diff options
| author | Vincent Laporte | 2019-03-13 07:42:00 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-13 07:42:00 +0000 |
| commit | e341c36cdc2aa2220152b2a3745bf3255316cdf3 (patch) | |
| tree | 2d9237639081c31e946c16671d3607cdfce0e760 /kernel/primred.ml | |
| parent | f1d60cad76439d96da36ed7c52ff71b1b9573b80 (diff) | |
| parent | ab1fd660db052741a3d9aed871251dc3dbee63ca (diff) | |
Merge PR #9627: Small retroknowledge/primitive cleanup
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: vbgl
Diffstat (limited to 'kernel/primred.ml')
| -rw-r--r-- | kernel/primred.ml | 4 |
1 files changed, 0 insertions, 4 deletions
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 |