Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.

Fixes #13266 (see #12675, 8641cb7385).

2 files changed, 30 insertions, 0 deletions

diff --git a/test-suite/output/bug_13266.out b/test-suite/output/bug_13266.out
new file mode 100644
index 0000000000..034830f1ac
--- /dev/null
+++ b/test-suite/output/bug_13266.out
@@ -0,0 +1,12 @@
+The command has indeed failed with message:
+Abstracting over the terms "S", "p" and "u" leads to a term
+fun (S0 : Type) (p0 : proc S0) (_ : S0) => p0 = Tick -> True
+which is ill-typed.
+Reason is: Illegal application: 
+The term "@eq" of type "forall A : Type, A -> A -> Prop"
+cannot be applied to the terms
+ "proc S0" : "Prop"
+ "p0" : "proc S0"
+ "Tick" : "proc unit"
+The 3rd term has type "proc unit" which should be coercible to 
+"proc S0".
diff --git a/test-suite/output/bug_13266.v b/test-suite/output/bug_13266.v
new file mode 100644
index 0000000000..e59455a326
--- /dev/null
+++ b/test-suite/output/bug_13266.v
@@ -0,0 +1,18 @@
+Inductive proc : Type -> Type :=
+| Tick : proc unit
+.
+
+Inductive exec :
+  forall T, proc T -> T -> Prop :=
+| ExecTick :
+    exec _ (Tick) tt
+.
+
+Lemma foo :
+  exec _ Tick tt ->
+  True.
+Proof.
+  intros H. 
+  remember Tick as p.
+  Fail induction H.
+Abort.