Merge PR #12499: Clean future goals

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot

2 files changed, 7 insertions, 11 deletions

diff --git a/test-suite/bugs/closed/bug_10939.v b/test-suite/bugs/closed/bug_10939.v
new file mode 100644
index 0000000000..e4adc35554
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10939.v
@@ -0,0 +1,5 @@
+Goal False.
+Proof.
+  epose proof ltac:(shelve). (* works *)
+  epose proof ltac:(admit). (* anomaly *)
+Abort.
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.