From e1f5a499c43ec0d7b7ebe696941217fb503e2596 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:09:29 +0200
Subject: Kernel: primitive projections handling of let-ins

Fixes bug #4176 (actually two bugs in one)

Correct computation of the type of primitive projections in presence of
let-ins.
---
 kernel/indtypes.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7774e52e9c..01acdce5c8 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,5 +43,5 @@ val is_indices_matter : unit -> bool
 
 val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.rel_context -> int array -> int array -> 
-  Context.rel_context -> 
+  Context.rel_context -> Context.rel_context -> 
   (constant array * projection_body array)
-- 
cgit v1.2.3