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/retyping.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'pretyping/retyping.ml') diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a56861c68..743bc3b19 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -127,13 +127,8 @@ let retype ?(polyprop=true) sigma = strip_outer_cast (subst_type env sigma (type_of env f) (Array.to_list args)) | Proj (p,c) -> - let Inductiveops.IndType(pars,realargs) = - let ty = type_of env c in - try Inductiveops.find_rectype env sigma ty - with Not_found -> retype_error BadRecursiveType - in - let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u)) + let ty = type_of env c in + Inductiveops.type_of_projection_knowing_arg env sigma p c ty | Cast (c,_, t) -> t | Sort _ | Prod _ -> mkSort (sort_of env cstr) -- cgit v1.2.3