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.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d480..90aa8000a8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -584,6 +584,15 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
       !evdref, mkArity (List.rev ctx,scl)
 
+let type_of_projection_knowing_arg env sigma p c ty =
+  let IndType(pars,realargs) =
+    try find_rectype env sigma ty
+    with Not_found ->
+      raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
+  in
+  let (_,u), pars = dest_ind_family pars in
+  substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+
 (***********************************************)
 (* Guard condition *)
 
-- 
cgit v1.2.3