From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 interp/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/declare.ml')

diff --git a/interp/declare.ml b/interp/declare.ml
index 4371b15c82..08a6ac5f7b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -370,7 +370,7 @@ let declare_projections univs mind =
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
   | PrimRecord info ->
-    let iter_ind i (_, labs, _) =
+    let iter_ind i (_, labs, _, _) =
       let ind = (mind, i) in
       let projs = Inductiveops.compute_projections env ind in
       Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
-- 
cgit v1.2.3