From fcfa1e90df70b7fc00a4865fb48c1dc3250c58d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Thu, 14 Aug 2014 14:14:25 +0200
Subject: Fix non-printing of coercions for primitive projections (fixes bug
 #3433).

---
 interp/constrextern.ml     | 24 +++++++++++++++++-------
 pretyping/inductiveops.ml  |  6 ++++++
 pretyping/inductiveops.mli |  4 ++++
 3 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 759410042..94c0dd47d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -530,15 +530,25 @@ let rec extern_args extern scopes env args subscopes =
 	  | scopt::subscopes -> (scopt,scopes), subscopes in
 	extern argscopes env a :: extern_args extern scopes env args subscopes
 
-let rec remove_coercions inctx = function
-  | GApp (loc,GRef (_,r,_),args) as c
-      when  not (!Flags.raw_print || !print_coercions)
-      ->
+
+let match_coercion_app = function
+  | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
+  | GProj (loc, r, arg) -> 
+    let pars = Inductiveops.projection_nparams r in
+      Some (loc, ConstRef r, pars, [arg])
+  | GApp (loc,GProj (_, r, c), args) -> 
+    let pars = Inductiveops.projection_nparams r in
+      Some (loc, ConstRef r, pars, c :: args)
+  | _ -> None
+
+let rec remove_coercions inctx c =
+  match match_coercion_app c with
+  | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
       let nargs = List.length args in
       (try match Classops.hide_coercion r with
-	  | Some n when n < nargs && (inctx || n+1 < nargs) ->
+	  | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
 	      (* We skip a coercion *)
-	      let l = List.skipn n args in
+	      let l = List.skipn (n - pars) args in
 	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
               (* Recursively remove the head coercions *)
 	      let a' = remove_coercions true a in
@@ -553,7 +563,7 @@ let rec remove_coercions inctx = function
 	      if List.is_empty l then a' else GApp (loc,a',l)
 	  | _ -> c
       with Not_found -> c)
-  | c -> c
+  | _ -> c
 
 let rec flatten_application = function
   | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l))
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5e853784e..34243f499 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
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1561cf97b..03d41015b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -121,6 +121,10 @@ val inductive_has_local_defs : inductive -> bool
 
 val allowed_sorts : env -> inductive -> sorts_family list
 
+(** Primitive projections *)
+val projection_nparams : projection -> int
+val projection_nparams_env : env -> projection -> int
+
 (** Extract information from an inductive family *)
 
 type constructor_summary = {
-- 
cgit v1.2.3