Properly handling projection parameters in canonical structures.

1 files changed, 8 insertions, 5 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 469b32eba..26b16c039 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -171,7 +171,7 @@ let keep_true_projections projs kinds =
   let filter (p, (_, b)) = if b then Some p else None in
   List.map_filter filter (List.combine projs kinds)
 
-let cs_pattern_of_constr t =
+let cs_pattern_of_constr env t =
   match kind_of_term t with
       App (f,vargs) ->
 	begin
@@ -181,7 +181,9 @@ let cs_pattern_of_constr t =
     | Rel n -> Default_cs, Some n, []
     | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
     | Proj (p, c) ->
-      Const_cs (ConstRef (Projection.constant p)), None, [c]
+      let { Environ.uj_type = ty } = Typeops.infer env c in
+      let _, params = Inductive.find_rectype env ty in
+      Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
     | Sort s -> Sort_cs (family_of_sort s), None, []
     | _ ->
 	begin
@@ -192,7 +194,6 @@ let cs_pattern_of_constr t =
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
          (fun (sign,env,t,con,proji_sp) ->
-          let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
           let env = Termops.push_rels_assum sign env in
           let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
@@ -209,14 +210,16 @@ let compute_canonical_projections warn (con,ind) =
   let v = (mkConstU (con,u)) in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+  let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
-  let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in
+  let lt = List.rev_map snd sign in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
   let params, projs = List.chop p args in
   let lpj = keep_true_projections lpj kl in
   let lps = List.combine lpj projs in
+  let nenv = Termops.push_rels_assum sign env in
   let comp =
     List.fold_left
       (fun l (spopt,t) -> (* comp=components *)
@@ -224,7 +227,7 @@ let compute_canonical_projections warn (con,ind) =
            | Some proji_sp ->
 	       begin
 		 try
-		   let patt, n , args = cs_pattern_of_constr t in
+		   let patt, n , args = cs_pattern_of_constr nenv t in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
                    if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);