Fixes in Ltac pattern-matching on primitive projections

and pretyping which was not contracting the eta-expanded forms in presence
of coercions.

2 files changed, 16 insertions, 13 deletions

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index d4cbad054..7af639633 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -229,7 +229,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	(match c1, kind_of_term c2 with
 	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) ->
 	  raise PatternMatchingFailure
-	  (* eta-expanded version of projection against projection *)
+	| PProj (pr1,c1), Proj (pr,c) ->
+	  if eq_constant pr1 pr then 
+	    try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2
+	    with Invalid_argument _ -> raise PatternMatchingFailure
+	  else raise PatternMatchingFailure
 	| _, Proj (pr,c) ->
 	  let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
 	    sorec stk env subst p term
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 93d65197b..5c18297c0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -563,6 +563,16 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	      with Not_found -> []
       else []
     in
+    let app_f = 
+      match kind_of_term fj.uj_val with
+      | Const (p, u) when Environ.is_projection p env ->
+	let pb = Environ.lookup_projection p env in
+	let npars = pb.Declarations.proj_npars in
+	  fun n -> 
+	    if n == npars + 1 then fun _ v -> mkProj (p, v)
+	    else fun f v -> applist (f, [v])
+      | _ -> fun _ f v -> applist (f, [v])
+    in
     let rec apply_rec env n resj candargs = function
       | [] -> resj
       | c::rest ->
@@ -581,7 +591,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 		  args, nf_evar !evdref (j_val hj)
 		else [], j_val hj
 	    in
-	    let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
+	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
 	    let j = { uj_val = value; uj_type = typ } in
 	      apply_rec env (n+1) j candargs rest
 		
@@ -604,17 +614,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in
 	    let t = Retyping.get_type_of env !evdref c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
-	  else if isConst f then
-	    let c,_ = destConst f in (* Internalize as primitive projection *)
-	      if is_projection c env then
-		let pb = lookup_projection c env in 
-		let npars = pb.Declarations.proj_npars and argslen = Array.length args in
-		  if npars < argslen then
-		    let proj = mkProj (c, args.(npars)) in
-		    let args = Array.sub args (npars+1) (argslen - (npars + 1)) in
-		      make_judge (mkApp (proj,args)) resj.uj_type
-		  else resj
-	      else resj
 	  else resj
       | _ -> resj 
     in