Expand the primitive functions on terms.

1 files changed, 14 insertions, 1 deletions

diff --git a/theories/Constr.v b/theories/Constr.v
index 801192d628..3e67a486cf 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -18,6 +18,8 @@ Module Unsafe.
 
 (** Low-level access to kernel terms. Use with care! *)
 
+Ltac2 Type case.
+
 Ltac2 Type kind := [
 | Rel (int)
 | Var (ident)
@@ -32,7 +34,7 @@ Ltac2 Type kind := [
 | Constant (constant, instance)
 | Ind (inductive, instance)
 | Constructor (constructor, instance)
-| Case (constr, constr, constr array)
+| Case (case, constr, constr, constr array)
 | Fix (int array, int, ident option array, constr array, constr array)
 | CoFix (int, ident option array, constr array, constr array)
 | Proj (projection, constr)
@@ -40,8 +42,19 @@ Ltac2 Type kind := [
 
 Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
 
+Ltac2 @ external make : kind -> constr := "ltac2" "constr_make".
+
+Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check".
+(** Checks that a constr generated by unsafe means is indeed safe in the
+    current environment, and returns it, or the error otherwise. Panics if
+    not focussed. *)
+
 Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl".
 (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with
     [r₁;...;rₙ] in [c]. *)
 
+Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "constr_closenl".
+(** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
+    [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
+
 End Unsafe.