From 9c2bbdd58b6935ea980e72289777a20b85fe4fdb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 19 Sep 2014 21:10:33 +0200
Subject: Fixes in Ltac pattern-matching on primitive projections and pretyping
 which was not contracting the eta-expanded forms in presence of coercions.

---
 pretyping/constrMatching.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping/constrMatching.ml')

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index d4cbad054e..7af6396336 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
-- 
cgit v1.2.3