From 8bf7221667dc2868027ed1080b3b70fd66144309 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 Dec 2014 14:13:01 +0100
Subject: Commits on evar-evar unification fixed HoTT_coq_106 and improved the
 status of #3278 (more precisely, it fixed a bug visible in the #3278 report,
 but a bug which arrived after #3278 was submitted).

---
 test-suite/bugs/opened/3278.v         | 2 +-
 test-suite/bugs/opened/HoTT_coq_106.v | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v
index 2c6d391a0c..ced535afd5 100644
--- a/test-suite/bugs/opened/3278.v
+++ b/test-suite/bugs/opened/3278.v
@@ -1,5 +1,5 @@
 Module a.
-  Fail Check let x' := _ in
+  Check let x' := _ in
              $(exact x')$.
 
   Notation foo x := (let x' := x in $(exact x')$).
diff --git a/test-suite/bugs/opened/HoTT_coq_106.v b/test-suite/bugs/opened/HoTT_coq_106.v
index 8d36abc0ed..a566459546 100644
--- a/test-suite/bugs/opened/HoTT_coq_106.v
+++ b/test-suite/bugs/opened/HoTT_coq_106.v
@@ -8,9 +8,10 @@ Instance ispointed_forall `{H : forall a : A, IsPointed (B a)}
 : IsPointed (forall a, B a)
   := fun a => @point (B a) (H a).
 
-Fail Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
+Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
 : IsPointed (sigT B).
-(* Toplevel input, characters 20-108:
+(* Message was at some time:
+Toplevel input, characters 20-108:
 Error: Unable to satisfy the following constraints:
 UNDEFINED EVARS:
  ?8==[A H B |- IsPointed (forall x : Type, ?13)] (parameter IsPointed of
-- 
cgit v1.2.3