From 1019a654a8262ee1b8b1e1a7f652a7e3d111d20e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 16:47:43 +0100
Subject: Fix test for #3848, still open.

---
 test-suite/bugs/opened/3848.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
index b66aeccaff..9413daa041 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/opened/3848.v
@@ -18,4 +18,4 @@ Proof.
   refine (functor_forall
             (f^-1)
             (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
-Defined. (* Error: Attempt to save an incomplete proof *)
+Fail Defined. (* Error: Attempt to save an incomplete proof *)
-- 
cgit v1.2.3