Two fixes in unification (bugs #3782 and #3709)

- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.

2 files changed, 86 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3709.v b/test-suite/bugs/closed/3709.v
new file mode 100644
index 0000000000..7f01be7abd
--- /dev/null
+++ b/test-suite/bugs/closed/3709.v
@@ -0,0 +1,23 @@
+Module NonPrim.
+  Unset Primitive Projections.
+  Record hProp := hp { hproptype :> Type }.
+  Goal forall (h : (Type -> hProp) -> (Type -> hProp)) k f,
+         (forall y, h y = y) ->
+         h (fun b : Type => {| hproptype := f b |}) = k.
+  Proof.
+    intros h k f H.
+    etransitivity.
+    apply H.
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record hProp := hp { hproptype :> Type }.
+  Goal forall (h : (Type -> hProp) -> (Type -> hProp)) k f,
+         (forall y, h y = y) ->
+         h (fun b : Type => {| hproptype := f b |}) = k.
+  Proof.
+    intros h k f H.
+    etransitivity.
+    apply H.
diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v
new file mode 100644
index 0000000000..08d456fc6d
--- /dev/null
+++ b/test-suite/bugs/closed/3782.v
@@ -0,0 +1,63 @@
+(* File reduced by coq-bug-finder from original input, then from 2674 lines to 136 lines, then from 115 lines to 61 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 28 2014 14:33:38 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,(no branch) (53bfe9cf58a3c40e6eb7120d25c1633a9cea3126) *)
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+Record Equiv A B := { equiv_fun : A -> B ; equiv_isequiv : IsEquiv equiv_fun }.
+Arguments equiv_fun {A B} _ _.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Set Printing Coercions.
+Set Printing Implicit.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record TruncType (n : nat) := { trunctype_type :> Type }.
+  Canonical Structure default_TruncType := fun n T => (@Build_TruncType n T).
+  Goal (forall (s d : TruncType 0) (m : trunctype_type 0 s -> trunctype_type 0 d),
+          @IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type) ->
+  forall (T T0 : Type) (m : T0 -> T), @IsEquiv T0 T m -> True.
+    intros isiso_isequiv' mc md e e'.
+    (pose (@isiso_isequiv'
+             _ _
+             (e
+              : (Build_TruncType 0 md) ->
+                (Build_TruncType 0 mc))
+             e') as i || fail "too early"); clear i.
+    pose (@isiso_isequiv'
+            _ _ _
+            e').
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record TruncType (n : nat) := { trunctype_type :> Type }.
+  Canonical Structure default_TruncType := fun n T => (@Build_TruncType n T).
+  Goal (forall (s d : TruncType 0) (m : trunctype_type 0 s -> trunctype_type 0 d),
+          @IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type) ->
+  forall (T T0 : Type) (m : T0 -> T), @IsEquiv T0 T m -> True.
+    intros isiso_isequiv' mc md e e'.
+    (pose (@isiso_isequiv'
+             _ _
+             (e
+              : (Build_TruncType 0 md) ->
+                (Build_TruncType 0 mc))
+             e') as i || fail "too early"); clear i.
+    Set Printing Existential Instances.
+    Set Debug Unification.
+    pose (@isiso_isequiv'
+            _ _ _
+            e'). (* Toplevel input, characters 48-50:
+Error:
+In environment
+isiso_isequiv' : forall (s d : TruncType 0)
+                   (m : trunctype_type 0 s -> trunctype_type 0 d),
+                 @IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type
+mc : Type
+md : Type
+e : md -> mc
+e' : @IsEquiv md mc e
+The term "e'" has type "@IsEquiv md mc e" while it is expected to have type
+ "@IsEquiv (trunctype_type 0 ?t) (trunctype_type 0 ?t0) ?t1".
+                  *)
+    admit.
+  Defined.
+End Prim.
\ No newline at end of file