Fix non-printing of coercions for primitive projections (fixes bug #3433).

1 files changed, 6 insertions, 0 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5e853784ec..34243f499c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -264,6 +264,12 @@ let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_kelim
 
+let projection_nparams_env env p = 
+  let pb = lookup_projection p env in
+    pb.proj_npars
+
+let projection_nparams p = projection_nparams_env (Global.env ()) p
+
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in