Adding a few primitive functions.

4 files changed, 19 insertions, 8 deletions

diff --git a/theories/Constr.v b/theories/Constr.v
index c340e3aa87..d7cd3b58a3 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -16,28 +16,28 @@ Ltac2 @ external equal : constr -> constr -> bool := "ltac2" "constr_equal".
 
 Module Unsafe.
 
-(** Low-level access to kernel term. Use with care! *)
+(** Low-level access to kernel terms. Use with care! *)
 
 Ltac2 Type kind := [
 | Rel (int)
 | Var (ident)
 | Meta (meta)
-| Evar (evar, constr list)
+| Evar (evar, constr array)
 | Sort (sort)
 | Cast (constr, cast, constr)
 | Prod (ident option, constr, constr)
 | Lambda (ident option, constr, constr)
 | LetIn (ident option, constr, constr, constr)
-| App (constr, constr list)
+| App (constr, constr array)
 | Constant (constant, instance)
 | Ind (inductive, instance)
 | Constructor (inductive, instance)
-(*
-  | Case      of case_info * 'constr * 'constr * 'constr array
-  | Fix       of ('constr, 'types) pfixpoint
-  | CoFix     of ('constr, 'types) pcofixpoint
-*)
+| 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)
 ].
 
+Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
+
 End Unsafe.
diff --git a/theories/Control.v b/theories/Control.v
index 3bc572547c..a6d46a89a8 100644
--- a/theories/Control.v
+++ b/theories/Control.v
@@ -21,6 +21,7 @@ Ltac2 @ external once : (unit -> 'a) -> 'a := "ltac2" "once".
 Ltac2 @ external dispatch : (unit -> unit) list -> unit := "ltac2" "dispatch".
 Ltac2 @ external extend : (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit := "ltac2" "extend".
 Ltac2 @ external enter : (unit -> unit) -> unit := "ltac2" "enter".
+Ltac2 @ external case : (unit -> 'a) -> ('a * (exn -> 'a)) result := "ltac2" "case".
 
 (** Proof state manipulation *)
 
@@ -44,6 +45,12 @@ Ltac2 @ external hyp : ident -> constr := "ltac2" "hyp".
     goal under focus, looks for the section variable with the given name.
     If there is one, looks for the hypothesis with the given name. *)
 
+Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "ltac2" "hyps".
+(** Panics if there is more than one goal under focus. If there is no
+    goal under focus, returns the list of section variables.
+    If there is one, returns the list of hypotheses. In both cases, the
+    list is ordered with rightmost values being last introduced. *)
+
 (** Refinement *)
 
 Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine".
diff --git a/theories/Init.v b/theories/Init.v
index 1d2d40f5c0..c0a73576d3 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -41,6 +41,8 @@ Ltac2 Type 'a ref := { mutable contents : 'a }.
 
 Ltac2 Type bool := [ true | false ].
 
+Ltac2 Type 'a result := [ Val ('a) | Err (exn) ].
+
 (** Pervasive exceptions *)
 
 Ltac2 Type exn ::= [ Out_of_bounds ].
diff --git a/theories/Message.v b/theories/Message.v
index b2159612cb..45f4b221db 100644
--- a/theories/Message.v
+++ b/theories/Message.v
@@ -14,6 +14,8 @@ Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string".
 
 Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int".
 
+Ltac2 @ external of_ident : ident -> message := "ltac2" "message_of_ident".
+
 Ltac2 @ external of_constr : constr -> message := "ltac2" "message_of_constr".
 (** Panics if there is more than one goal under focus. *)