From 2420764db089d731635787bc11bd9ab312250fe7 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter
Date: Fri, 19 Mar 2021 16:31:35 -0400
Subject: implement is_const, is_var, ... etc and has_evar for Ltac2

Fixes #13963
---
 test-suite/ltac2/evar.v   | 17 +++++++++++++++++
 test-suite/ltac2/rebind.v |  4 +---
 2 files changed, 18 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/ltac2/evar.v

(limited to 'test-suite')

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.
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index 7b3a460c8c..9108871e28 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -26,12 +26,10 @@ Ltac2 rec nat_eq n m :=
   | S n => match m with | O => false | S m => nat_eq n m end
   end.
 
-Ltac2 Type exn ::= [ Assertion_failed ].
-
 Ltac2 assert_eq n m :=
   match nat_eq n m with
   | true => ()
-  | false => Control.throw Assertion_failed end.
+  | false => Control.throw Assertion_failure end.
 
 Ltac2 mutable x := O.
 Ltac2 y := x.
-- 
cgit v1.2.3