diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-07-22 17:18:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-07-22 17:18:17 +0200 |
| commit | c07a9f1e558ab55de3011cbfc9749391ed60c768 (patch) | |
| tree | 1a376435c4d2b1c0ff5ce2ba9c3534233ccd1976 /kernel/cemitcodes.ml | |
| parent | 246a5011d7a794835aa0f9ca198b3a4a74031ed6 (diff) | |
Fix incomplete pattern-matching.
I was not seeing the warning due to the 10 deprecation warnings before
it...
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 0d9334a50..6dbfbe9cc 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -308,6 +308,7 @@ type to_patch = emitcodes * (patch list) * fv let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> 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,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) |