diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-27 13:54:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-27 14:03:59 +0100 |
| commit | cbd815a289db52f58235f23f5afba3be49cc8eed (patch) | |
| tree | 3e75c7e36206be429ad3f81b9551d02865599eeb /kernel/cemitcodes.ml | |
| parent | 77e6eda6388aba117476f6c8445c4b61ebdbc33e (diff) | |
Removing dead code.
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 5ba93eda0..61042ccc1 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -306,8 +306,6 @@ let init () = type emitcodes = string -let copy = String.copy - let length = String.length type to_patch = emitcodes * (patch list) * fv @@ -332,8 +330,6 @@ let subst_patch s (ri,pos) = let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv -let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) - type body_code = | BCdefined of to_patch | BCalias of Names.constant |