Fix semantics of matching with folded/unfolded projections to definitely

avoid looping and be compatible with unfold.

4 files changed, 17 insertions, 15 deletions

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index b0f1dd920a..270d274778 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -220,37 +220,37 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
             Array.fold_left2 (sorec stk env) subst args1 args22
           else (* Might be a projection on the right *)
 	    match kind_of_term c2 with
-	    | Proj (pr, c) ->
+	    | Proj (pr, c) when not (Projection.unfolded pr) ->
 	      let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
 		sorec stk env subst p term
 	    | _ -> raise PatternMatchingFailure)
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
 	(match c1, kind_of_term c2 with
-	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) ->
+	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr))
+	    || Projection.unfolded pr ->
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
-	  if eq_constant (Projection.constant pr1) (Projection.constant pr) then 
+	  if Projection.equal 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) ->
+	| _, Proj (pr,c) when not (Projection.unfolded pr) ->
 	  let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
 	    sorec stk env subst p term
 	| _, _ ->
           try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
-      | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 
-								(Projection.constant pr)) -> 
+      | PApp (PRef (ConstRef c1), _), Proj (pr, c2) 
+	when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> 
 	raise PatternMatchingFailure
 	
       | PApp (c, args), Proj (pr, c2) ->
 	let term = Retyping.expand_projection env sigma pr c2 [] in
 	  sorec stk env subst p term
 
-      | PProj (p1,c1), Proj (p2,c2) when 
-	  eq_constant (Projection.constant p1) (Projection.constant p2) ->
+      | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
           sorec stk env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ab04a90459..bddd274efa 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -799,9 +799,6 @@ and whd_construct_stack env sigma s =
    sequence of products; fails if no delta redex is around
 *)
 
-let match_eval_proj env proj =
-  ((lookup_constant proj env).Declarations.const_proj)
-
 let try_red_product env sigma c =
   let simpfun = clos_norm_flags betaiotazeta env sigma in
   let rec redrec env x =
diff --git a/test-suite/bugs/closed/3656.v b/test-suite/bugs/closed/3656.v
index 218cb755b2..cbd773d079 100644
--- a/test-suite/bugs/closed/3656.v
+++ b/test-suite/bugs/closed/3656.v
@@ -26,7 +26,7 @@ Ltac head_hnf_under_binders x :=
     | ?y => y
   end.
 Goal forall s : @hSet nat, True.
-intros. 
+intros.
 let x := head_hnf_under_binders setT in pose x.
 
 set (foo := eq_refl (@setT nat)). generalize foo. simpl. cbn. 
@@ -42,8 +42,12 @@ Ltac head_hnf_under_binders x :=
     | ?y => y
   end.
 Goal setT = setT.
- Fail progress unfold setT. (* should not succeed *)
+ progress unfold setT. (* should not succeed *)
  match goal with
     | |- (fun h => setT h) = (fun h => setT h) => fail 1 "should not eta-expand"
     | _ => idtac
-  end. (* should not fail *)
\ No newline at end of file
+  end. (* should not fail *)
+Abort.
+
+Goal forall h, setT h = setT h.
+Proof. intro. progress unfold setT. 
diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
index 0de92b131e..753fb33ca2 100644
--- a/test-suite/bugs/closed/3662.v
+++ b/test-suite/bugs/closed/3662.v
@@ -44,4 +44,5 @@ Goal forall x : prod nat nat, fst x = 0.
   match goal with
     | [ |- fst ?x = 0 ] => idtac
   end.
-Abort.
\ No newline at end of file
+Abort.
+