From a51cce369b9c634a93120092d4c7685a242d55b1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 4 Jul 2015 14:22:08 +0200
Subject: Fix handling of primitive projections in VM.

I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
---
 pretyping/inductiveops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/inductiveops.mli')

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7959759a3f..757599a3ce 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,6 +126,8 @@ val allowed_sorts : env -> inductive -> sorts_family list
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
+val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
+  constr -> types -> types
 
 (** Extract information from an inductive family *)
 
-- 
cgit v1.2.3