From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 kernel/nativecode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f30ddce4d7..c8cee7db73 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2088,7 +2088,7 @@ let compile_deps env sigma prefix ~interactive init t =
   | Proj (p,c) ->
     let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
     aux env lvl init c
-  | Case (ci, _p, _c, _ac) ->
+  | Case (ci, _p, _iv, _c, _ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
       fold_constr_with_binders succ (aux env) lvl init t
-- 
cgit v1.2.3