1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/ltac2/evar.v b/test-suite/ltac2/evar.v
new file mode 100644
index 0000000000..2c82673edd
--- /dev/null
+++ b/test-suite/ltac2/evar.v
@@ -0,0 +1,17 @@
+Require Import Ltac2.Ltac2.
+
+Goal exists (a: nat), a = 1.
+Proof.
+  match! goal with
+  | [ |- ?g ] => Control.assert_false (Constr.has_evar g)
+  end.
+  eexists.
+  match! goal with
+  | [ |- ?g ] => Control.assert_true (Constr.has_evar g)
+  end.
+  match! goal with
+  | [ |- ?x = ?y ] =>
+    Control.assert_true (Constr.is_evar x);
+    Control.assert_false (Constr.is_evar y)
+  end.
+Abort.