There are some occurs-check cases that can be handled by imitation (using pruning),

hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but
backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).

3 files changed, 91 insertions, 10 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 23358bab5..04c69d74a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -319,19 +319,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 	   destroy beta-redexes that can be used for 1st-order unification *)
         let term1 = apprec_nohdbeta ts env evd term1 in
         let term2 = apprec_nohdbeta ts env evd term2 in
-        begin match kind_of_term term1, kind_of_term term2 with
-        | Evar ev, _ when Evd.is_undefined evd (fst ev)
-	&& noccur_evar env evd (fst ev) term2 ->
-          solve_simple_eqn (evar_conv_x ts) env evd
-            (position_problem true pbty,ev,term2)
-        | _, Evar ev when Evd.is_undefined evd (fst ev)
-	&& noccur_evar env evd (fst ev) term1 ->
-          solve_simple_eqn (evar_conv_x ts) env evd
-            (position_problem false pbty,ev,term1)
-        | _ ->
+	let default () = 
           evar_eqappr_x ts env evd pbty
             (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
             (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
+	in
+          begin match kind_of_term term1, kind_of_term term2 with
+          | Evar ev, _ when Evd.is_undefined evd (fst ev) ->
+            (match solve_simple_eqn (evar_conv_x ts) env evd
+              (position_problem true pbty,ev,term2) with
+	      | UnifFailure (_,OccurCheck _) -> 
+		(* Eta-expansion might apply *) default ()
+	      | x -> x)
+          | _, Evar ev when Evd.is_undefined evd (fst ev) ->
+            (match solve_simple_eqn (evar_conv_x ts) env evd
+              (position_problem false pbty,ev,term1) with
+	      | UnifFailure (_, OccurCheck _) ->
+		(* Eta-expansion might apply *) default () 
+	      | x -> x)
+          | _ -> default ()
         end
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
diff --git a/test-suite/bugs/closed/3477.v b/test-suite/bugs/closed/3477.v
new file mode 100644
index 000000000..e94148647
--- /dev/null
+++ b/test-suite/bugs/closed/3477.v
@@ -0,0 +1,9 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall A B : Set, True.
+Proof.
+  intros A B.
+  evar (a : prod A B); evar (f : (prod A B -> Set)).
+  let a' := (eval unfold a in a) in
+  set(foo:=eq_refl : a' = (@pair _ _ (fst a') (snd a'))).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v
new file mode 100644
index 000000000..c862965d4
--- /dev/null
+++ b/test-suite/bugs/closed/3539.v
@@ -0,0 +1,66 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-no-native-compiler") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *)
+(* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *)
+
+Set Implicit Arguments.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Local Set Primitive Projections.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+Axiom path_prod : forall {A B : Type} (z z' : A * B), (fst z = fst z') -> (snd z = snd z') -> (z = z').
+Axiom transport_path_prod : forall A B (P : A * B -> Type) (x y : A * B) (HA : fst x = fst y) (HB : snd x = snd y) Px,
+                              transport P (path_prod _ _ HA HB) Px
+                              = transport (fun x => P (x, snd y)) HA (transport (fun y => P (fst x, y)) HB Px).
+Goal forall (T0 : Type) (snd1 snd0 f : T0) (p : @paths T0 f snd0)
+            (f0 : T0) (p1 : @paths T0 f0 snd1) (T1 : Type)
+            (fst1 fst0 : T1) (p0 : @paths T1 fst0 fst0) (p2 : @paths T1 fst1 fst1)
+            (T : Type) (x2 : T) (T2 : Type) (T3 : forall (_ : T2) (_ : T2), Type)
+            (x' : forall (_ : T1) (_ : T), T2) (m : T3 (x' fst1 x2) (x' fst0 x2)),
+       @paths (T3 (x' fst1 x2) (x' fst0 x2))
+              (@transport (prod T1 T0)
+                          (fun x : prod T1 T0 =>
+                             T3 (x' fst1 x2) (x' (fst x) x2))
+                          (@pair T1 T0 fst0 f) (@pair T1 T0 fst0 snd0)
+                          (@path_prod T1 T0 (@pair T1 T0 fst0 f)
+                                      (@pair T1 T0 fst0 snd0) p0 p)
+                          (@transport (prod T1 T0)
+                                      (fun x : prod T1 T0 =>
+                                         T3 (x' (fst x) x2) (x' fst0 x2))
+                                      (@pair T1 T0 fst1 f0) (@pair T1 T0 fst1 snd1)
+                                      (@path_prod T1 T0 (@pair T1 T0 fst1 f0)
+                                                  (@pair T1 T0 fst1 snd1) p2 p1) m)) m.
+  intros.
+  match goal with
+    | [ |- context[transport ?P (path_prod ?x ?y ?HA ?HB) ?Px] ]
+      => rewrite (transport_path_prod P x y HA HB Px)
+  end || fail "bad".
+  Undo.
+  Set Printing All.
+  rewrite transport_path_prod. (* Toplevel input, characters 15-43:
+Error:
+In environment
+T0 : Type
+snd1 : T0
+snd0 : T0
+f : T0
+p : @paths T0 f snd0
+f0 : T0
+p1 : @paths T0 f0 snd1
+T1 : Type
+fst1 : T1
+fst0 : T1
+p0 : @paths T1 fst0 fst0
+p2 : @paths T1 fst1 fst1
+T : Type
+x2 : T
+T2 : Type
+T3 : forall (_ : T2) (_ : T2), Type
+x' : forall (_ : T1) (_ : T), T2
+m : T3 (x' fst1 x2) (x' fst0 x2)
+Unable to unify "?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with
+"?25 ?27".
+ *)
\ No newline at end of file