Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2

Reviewed-by: ppedrot

2 files changed, 18 insertions, 3 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.
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.