Adding a few primitive functions.

1 files changed, 7 insertions, 0 deletions

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".