From c6529d84b9587de4b10bb0ba5ca0ec138d0f2a91 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Nov 2020 20:45:31 +0100
Subject: Fixes #13363: case of a meta not paying attention to being under
 binders.

In Evar := C[Meta] problems of unification.ml, and C[ ] contains
binders, Meta was wrongly considered by pose_all_metas_as_evars as
under these binders (while Metas are always defined in the initial
context of the unification problem).
---
 test-suite/bugs/closed/bug_13363.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13363.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_13363.v b/test-suite/bugs/closed/bug_13363.v
new file mode 100644
index 0000000000..cc11aa93b6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13363.v
@@ -0,0 +1,17 @@
+Axiom X : Type.       
+Axiom P : (X -> unit) -> Prop.
+
+Axiom F: unit -> unit.
+Axiom G : unit -> unit.
+
+Lemma Hyp ss':
+    P (fun y : X => ss') ->
+    P (fun y : X => G (F ss')).
+Admitted.
+
+Lemma bug : exists x, P x.
+Proof.
+intros.
+eexists (fun y : X => G _).
+eapply Hyp. cbn beta.
+Abort.
-- 
cgit v1.2.3