Reenable FO unification of primitive projections and their eta-expanded

forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.

3 files changed, 59 insertions, 12 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 21629553d..799ca2523 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -572,7 +572,29 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
-
+	      
+	(* Catch the p.c ~= p c' cases *)
+	| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
+	  let res = 
+	    try Some (destApp (Retyping.expand_projection env evd p c []))
+	    with Retyping.RetypeError _ -> None
+	  in
+	    (match res with 
+	    | Some (f1,args1) -> 
+	      evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) 
+		(appr2,csts2)
+	    | None -> UnifFailure (evd,NotSameHead))
+	      
+	| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
+	  let res = 
+	    try Some (destApp (Retyping.expand_projection env evd p' c' []))
+	    with Retyping.RetypeError _ -> None
+	  in 
+	    (match res with
+	    | Some (f2,args2) ->
+	      evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2)
+	    | None -> UnifFailure (evd,NotSameHead))
+	      
 	| _, _ ->
 	let f1 i = 
 	  (* Gather the universe constraints that would make term1 and term2 equal.
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2b6c3921e..527199e3b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -678,17 +678,31 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 
 	(* For records *)
 	| App (f1, l1), _ when flags.modulo_eta && 
+	    (* This ensures cN is an evar, meta or irreducible constant/variable
+	       and not a constructor. *)
 	    is_eta_constructor_app curenv flags.modulo_delta f1 l1 cN ->
-	  let l1', l2' = eta_constructor_app curenv f1 l1 cN in
-	  let opt' = {opt with at_top = true; with_cs = false} in
-	    Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
+	  (try 
+	     let l1', l2' = eta_constructor_app curenv f1 l1 cN in
+	     let opt' = {opt with at_top = true; with_cs = false} in
+	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
+	   with ex when precatchable_exception ex ->
+	     match kind_of_term cN with
+	     | App(f2,l2) when isMeta f2 || isEvar f2 ->
+	       unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	     | _ -> raise ex)
 
 	| _, App (f2, l2) when flags.modulo_eta && 
 	    is_eta_constructor_app curenv flags.modulo_delta f2 l2 cM ->
-	  let l2', l1' = eta_constructor_app curenv f2 l2 cM in
-	  let opt' = {opt with at_top = true; with_cs = false} in
-	    Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
-	   
+	  (try 
+	     let l2', l1' = eta_constructor_app curenv f2 l2 cM in
+	     let opt' = {opt with at_top = true; with_cs = false} in
+	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
+	   with ex when precatchable_exception ex ->
+	     match kind_of_term cM with
+	     | App(f1,l1) when isMeta f1 || isEvar f1 ->
+	       unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	     | _ -> raise ex)
+
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             (try 
 	     let opt' = {opt with at_top = true; with_types = false} in
@@ -729,9 +743,15 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 
 	| App (f1,l1), App (f2,l2) ->
 	  unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	    
+	| App (f1,l1), Proj(p2,c2) ->
+	  unify_app curenvnb pb opt substn cM f1 l1 cN cN [||]
+
+	| Proj (p1,c1), App(f2,l2) ->
+	  unify_app curenvnb pb opt substn cM cM [||] cN f2 l2
 
 	| _ ->
-            unify_not_same_head curenvnb pb opt substn cM cN
+          unify_not_same_head curenvnb pb opt substn cM cN
 
   and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
     try
@@ -756,8 +776,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       let opta = {opt with at_top = true; with_types = false} in
       let optf = {opt with at_top = true; with_types = true} in
       let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
-	Array.fold_left2 (unirec_rec curenvnb CONV opta)
-	  (unirec_rec curenvnb CONV optf substn f1 f2) l1 l2
+	if Array.length l1 == 0 then error_cannot_unify (fst curenvnb) sigma (cM,cN)
+	else
+	  Array.fold_left2 (unirec_rec curenvnb CONV opta)
+	    (unirec_rec curenvnb CONV optf substn f1 f2) l1 l2
     with ex when precatchable_exception ex ->
     try reduce curenvnb pb {opt with with_types = false} substn cM cN
     with ex when precatchable_exception ex ->
diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v
index 3070a4128..6c40a4266 100644
--- a/test-suite/bugs/closed/3484.v
+++ b/test-suite/bugs/closed/3484.v
@@ -14,7 +14,10 @@ Proof.
   apply (@ap _ _ pr1 _ y).
   Undo.
   Unset Printing Notations.
-  apply (ap pr1). admit. 
+  apply (ap pr1). 
+  Undo.
+  refine (ap pr1 _).
+admit. 
 Defined.
 
 (* Toplevel input, characters 22-28: