Fix evarconv not applying eta when it used to. Fixes bug#3319.

2 files changed, 20 insertions, 23 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ca0644c47e..53b4526c2c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -396,21 +396,21 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ise_try evd [f1; (consume_stack on_left apprF apprM); f3] in
   let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
     let switch f a b = if on_left then f a b else f b a in
-    match Stack.list_of_app_stack skF with
+    let f1 evd = 
+      match Stack.list_of_app_stack skF with
       | None -> consume_stack on_left apprF apprR evd
       | Some lF ->
-	let f1 evd =
-	  miller_pfenning on_left
-	    (fun () -> (* Postpone the use of an heuristic *)
-	      switch (fun x y ->
-		Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR)
-	    ev lF apprR evd
-	and f2 evd =
-	  if isLambda termR then
-	    eta env evd false skR termR skF termF
-	  else UnifFailure (evd,NotSameHead)
-	in ise_try evd [f1;f2] in
-
+	miller_pfenning on_left
+	  (fun () -> (* Postpone the use of an heuristic *)
+	    switch (fun x y ->
+	      Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR)
+	  ev lF apprR evd
+    in
+    let f2 evd =
+      if isLambda termR then
+	eta env evd false skR termR skF termF
+      else UnifFailure (evd,NotSameHead)
+    in ise_try evd [f1;f2] in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
diff --git a/test-suite/bugs/opened/3319.v b/test-suite/bugs/closed/3319.v
index 7851a08ea4..bb5853ddd3 100644
--- a/test-suite/bugs/opened/3319.v
+++ b/test-suite/bugs/closed/3319.v
@@ -3,6 +3,7 @@ Set Implicit Arguments.
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a
                  where "x = y" := (@paths _ x y) : type_scope.
+
 Record PreCategory := { obj :> Type; morphism : obj -> obj -> Type }.
 Record NotionOfStructure (X : PreCategory) :=
   { structure :> X -> Type;
@@ -14,15 +15,11 @@ Section precategory.
   Variable P : NotionOfStructure X.
   Local Notation object := { x : X & P x }.
   Record morphism' (xa yb : object) := {}.
-  Fail Lemma issig_morphism xa yb
+
+  Lemma issig_morphism xa yb
   : { f : morphism X (projT1 xa) (projT1 yb)
     & is_structure_homomorphism _ _ _ f (projT2 xa) (projT2 yb) }
-    = morphism' xa yb. (* Toplevel input, characters 169-171:
-Error:
-In environment
-X : PreCategory
-P : NotionOfStructure X
-xa : {x : _ & ?26 x}
-yb : {x : _ & ?26 x}
-The term "xa" has type "{x : _ & ?26 x}" while it is expected to have type
- "{x : X & P x}". *)
+    = morphism' xa yb. 
+  Proof.
+    admit.
+  Defined.
\ No newline at end of file