diff options
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2a70d0b1b..ef0c9af4f 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -307,7 +307,7 @@ type to_patch = emitcodes * (patch list) * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ -> sc + | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) |