Exporting more internals from Coq implementation.

2 files changed, 49 insertions, 9 deletions

diff --git a/theories/Control.v b/theories/Control.v
index a6d46a89a8..a8b92aced2 100644
--- a/theories/Control.v
+++ b/theories/Control.v
@@ -54,3 +54,10 @@ Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "ltac2"
 (** Refinement *)
 
 Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine".
+
+(** Evars *)
+
+Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "ltac2" "with_holes".
+(** [with_holes x f] evaluates [x], then apply [f] to the result, and fails if
+    all evars generated by the call to [x] have not been solved when [f]
+    returns. *)
diff --git a/theories/Std.v b/theories/Std.v
index 5cc1622ba9..a9eced6cbb 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -8,8 +8,39 @@
 
 Require Import Ltac2.Init.
 
+(** ML-facing types *)
+
+Ltac2 Type hypothesis := [ AnonHyp (int) | NamedHyp (ident) ].
+
+Ltac2 Type bindings := [
+| NoBindings
+| ImplicitBindings (constr list)
+| ExplicitBindings ((hypothesis * constr) list)
+].
+
+Ltac2 Type constr_with_bindings := constr * bindings.
+
+Ltac2 Type occurrences := [
+| AllOccurrences
+| AllOccurrencesBut (int list)
+| NoOccurrences
+| OnlyOccurrences (int list)
+].
+
+Ltac2 Type hyp_location_flag := [ InHyp | InHypTypeOnly | InHypValueOnly ].
+
+Ltac2 Type clause := {
+  on_hyps : (ident * occurrences * hyp_location_flag) list option;
+  on_concl : occurrences;
+}.
+
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
+Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim".
+Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".
+
+Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize".
+
 Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity".
 
 Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption".
@@ -20,20 +51,22 @@ Ltac2 @ external etransitivity : unit -> unit := "ltac2" "tac_etransitivity".
 
 Ltac2 @ external cut : constr -> unit := "ltac2" "tac_cut".
 
-Ltac2 @ external left : unit -> unit := "ltac2" "tac_left".
-Ltac2 @ external eleft : unit -> unit := "ltac2" "tac_eleft".
-Ltac2 @ external right : unit -> unit := "ltac2" "tac_right".
-Ltac2 @ external eright : unit -> unit := "ltac2" "tac_eright".
+Ltac2 @ external left : bindings -> unit := "ltac2" "tac_left".
+Ltac2 @ external eleft : bindings -> unit := "ltac2" "tac_eleft".
+Ltac2 @ external right : bindings -> unit := "ltac2" "tac_right".
+Ltac2 @ external eright : bindings -> unit := "ltac2" "tac_eright".
 
 Ltac2 @ external constructor : unit -> unit := "ltac2" "tac_constructor".
 Ltac2 @ external econstructor : unit -> unit := "ltac2" "tac_econstructor".
-Ltac2 @ external split : unit -> unit := "ltac2" "tac_split".
-Ltac2 @ external esplit : unit -> unit := "ltac2" "tac_esplit".
+Ltac2 @ external split : bindings -> unit := "ltac2" "tac_split".
+Ltac2 @ external esplit : bindings -> unit := "ltac2" "tac_esplit".
+
+Ltac2 @ external constructor_n : int -> bindings -> unit := "ltac2" "tac_constructorn".
+Ltac2 @ external econstructor_n : int -> bindings -> unit := "ltac2" "tac_econstructorn".
 
-Ltac2 @ external constructor_n : int -> unit := "ltac2" "tac_constructorn".
-Ltac2 @ external econstructor_n : int -> unit := "ltac2" "tac_econstructorn".
+Ltac2 @ external intros_until : hypothesis -> unit := "ltac2" "tac_introsuntil".
 
-Ltac2 @ external symmetry : unit -> unit := "ltac2" "tac_symmetry".
+Ltac2 @ external symmetry : clause -> unit := "ltac2" "tac_symmetry".
 
 Ltac2 @ external rename : (ident * ident) list -> unit := "ltac2" "tac_rename".