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/vnorm.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/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 8198db1b8..af640d7f3 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -216,6 +216,10 @@ and nf_stk env c t stk = let tcase = build_case_type dep p realargs c in let ci = case_info sw in nf_stk env (mkCase(ci, p, c, branchs)) tcase stk + | Zproj p :: stk -> + let p' = Projection.make p true in + let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in + nf_stk env (mkProj(p',c)) ty stk and nf_predicate env ind mip params v pT = match whd_val v, kind_of_term pT with |