diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-04 14:22:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-05 02:00:07 +0200 |
| commit | a51cce369b9c634a93120092d4c7685a242d55b1 (patch) | |
| tree | dd68ea8dadf86f9a6eb400839f515ed5b9cf8f95 /pretyping/retyping.ml | |
| parent | 31c7542731a62f56bd60f443a84d68813f8780a8 (diff) | |
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.
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 9 |
1 files changed, 2 insertions, 7 deletions
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) |