Merge branch 'v8.5' into trunk

5 files changed, 18 insertions, 8 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d48..90aa8000a 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 *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7959759a3..757599a3c 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 *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 436f61d7b..b59589bda 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,7 +1,7 @@
 Locusops
 Reductionops
-Vnorm
 Inductiveops
+Vnorm
 Arguments_renaming
 Nativenorm
 Retyping
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)
 
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