From c07a9f1e558ab55de3011cbfc9749391ed60c768 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Wed, 22 Jul 2015 17:18:17 +0200
Subject: Fix incomplete pattern-matching.

I was not seeing the warning due to the 10 deprecation warnings before
it...
---
 kernel/cemitcodes.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/cemitcodes.ml')

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)
 
-- 
cgit v1.2.3