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/mod_subst.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/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? |