From 6c2a5cba55a831e461e806e08c7be968f9343f7e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 12 Jun 2020 01:18:27 +0200
Subject: Make future_goals stack explicit in the evarmap

---
 test-suite/bugs/closed/bug_4095.v | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v
index 3d3015c383..d667022e68 100644
--- a/test-suite/bugs/closed/bug_4095.v
+++ b/test-suite/bugs/closed/bug_4095.v
@@ -71,18 +71,9 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     refine (P _ _)
   end.
   Undo.
-  Fail lazymatch goal with
+  lazymatch goal with
   | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
     let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
     set(p:=P)
-  end. (* Toplevel input, characters 15-182:
-Error: Cannot infer an instance of type
-"PointedOPred" for the variable p in environment:
-T : Type
-O0 : T -> OPred
-O1 : T -> PointedOPred
-tr : T -> T
-O2 : PointedOPred
-x0 : T
-H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
+  end.
 Abort.
-- 
cgit v1.2.3