5 files changed, 76 insertions, 6 deletions
diff --git a/test-suite/interactive/ParalITP_fail_on_qed.v b/test-suite/interactive/ParalITP_fail_on_qed.v
new file mode 100644
index 0000000000..37692ed254
--- /dev/null
+++ b/test-suite/interactive/ParalITP_fail_on_qed.v
@@ -0,0 +1,54 @@
+(* Some boilerplate *)
+Fixpoint fib n := match n with
+  | O => 1
+  | S m => match m with
+    | O => 1
+    | S o => fib o + fib m end end.
+
+Ltac sleep n :=
+  try (cut (fib n = S (fib n)); reflexivity).
+
+(* Tune that depending on your PC *)
+Let time := 10.
+
+
+(* Beginning of demo *)
+
+Section Demo.
+
+Variable i : True.
+
+Lemma a (n : nat) : nat.
+Proof using.
+  revert n.
+  fix f 1.
+  apply f.
+Qed.
+
+Lemma b : True.
+Proof using i.
+  sleep time.
+  idtac.
+  sleep time.
+  (* Here we use "a" *)
+  exact I.
+Qed.
+
+Lemma work_here : True /\ True.
+Proof using i.
+(* Jump directly here, Coq reacts immediately *)
+split.
+  exact b.  (* We can use the lemmas above *)
+exact I.
+Qed.
+
+End Demo.
+
+From Coq Require Import Program.Tactics.
+Obligation Tactic := idtac.
+Program Definition foo : nat -> nat * nat :=
+  fix f (n : nat) := (0,_).
+
+Next Obligation.
+intros f n; apply (f n).
+Qed.
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 4c0ee1b5bd..767b3c1922 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -23,11 +23,11 @@ Module Pair (X: PO) (Y: PO) <: PO.
   Hint Unfold le.
 
   Lemma le_refl : forall p : T, le p p.
-    info auto.
+    auto.
   Qed.
 
   Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
-    unfold le;  intuition; info  eauto.
+    unfold le;  intuition; eauto.
   Qed.
 
   Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
@@ -39,9 +39,9 @@ Module Pair (X: PO) (Y: PO) <: PO.
      enough (t0 = t2) as ->.
     reflexivity.
 
-    info auto.
+    auto.
 
-    info auto.
+    auto.
   Qed.
 
 End Pair.
@@ -53,5 +53,5 @@ Require Nat.
 Module NN := Pair Nat Nat.
 
 Lemma zz_min : forall p : NN.T, NN.le (0, 0) p.
-  info auto with arith.
+  auto with arith.
 Qed.
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
index 92917cdfc7..7b295dd1cb 100644
--- a/test-suite/output/auto.v
+++ b/test-suite/output/auto.v
@@ -1,4 +1,4 @@
-(* testing info/debug auto/eauto *)
+(* testing info_*/debug auto/eauto *)
 
 Goal False \/ (True -> True).
 info_auto.
diff --git a/test-suite/output/bug12442.out b/test-suite/output/bug12442.out
new file mode 100644
index 0000000000..644ef6cd7c
--- /dev/null
+++ b/test-suite/output/bug12442.out
@@ -0,0 +1,6 @@
+The command has indeed failed with message:
+No product even after head-reduction.
+The command has indeed failed with message:
+Not an inductive product.
+The command has indeed failed with message:
+Not an inductive product.
diff --git a/test-suite/output/bug12442.v b/test-suite/output/bug12442.v
new file mode 100644
index 0000000000..481989a4e9
--- /dev/null
+++ b/test-suite/output/bug12442.v
@@ -0,0 +1,10 @@
+Parameter A B : Prop.
+Axiom P : inhabited (A -> B).
+
+Goal A -> True.
+Proof.
+  Fail intros ?%P ?.
+  Fail intros []%P.
+  intro a.
+  Fail apply P in a as [].
+Abort.