implement is_const, is_var, ... etc and has_evar for Ltac2

Fixes #13963

1 files changed, 51 insertions, 0 deletions

diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 72cac900cd..fa056910b8 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -96,3 +96,54 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "lt
 
 Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype".
 (** Pretype the provided preterm. Assumes the goal to be focussed. *)
+
+
+Ltac2 is_evar(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Evar _ _ => true
+  | _ => false
+  end.
+
+Ltac2 @ external has_evar : constr -> bool := "ltac2" "constr_has_evar".
+
+Ltac2 is_var(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Var _ => true
+  | _ => false
+  end.
+
+Ltac2 is_fix(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Fix _ _ _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_cofix(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.CoFix _ _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_ind(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Ind _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_constructor(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Constructor _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_proj(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Proj _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_const(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Constant _ _ => true
+  | _ => false
+  end.