Turning the ltac2 subfolder into a standalone plugin.

1 files changed, 49 insertions, 0 deletions

diff --git a/theories/Control.v b/theories/Control.v
new file mode 100644
index 0000000000..3bc572547c
--- /dev/null
+++ b/theories/Control.v
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+(** Panic *)
+
+Ltac2 @ external throw : exn -> 'a := "ltac2" "throw".
+(** Fatal exception throwing. This does not induce backtracking. *)
+
+(** Generic backtracking control *)
+
+Ltac2 @ external zero : exn -> 'a := "ltac2" "zero".
+Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "ltac2" "plus".
+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".
+
+(** Proof state manipulation *)
+
+Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "ltac2" "focus".
+Ltac2 @ external shelve : unit -> unit := "ltac2" "shelve".
+Ltac2 @ external shelve_unifiable : unit -> unit := "ltac2" "shelve_unifiable".
+
+Ltac2 @ external new_goal : evar -> unit := "ltac2" "new_goal".
+(** Adds the given evar to the list of goals as the last one. If it is
+    already defined in the current state, don't do anything. Panics if the
+    evar is not in the current state. *)
+
+(** Goal inspection *)
+
+Ltac2 @ external goal : unit -> constr := "ltac2" "goal".
+(** Panics if there is not exactly one goal under focus. Otherwise returns
+    the conclusion of this goal. *)
+
+Ltac2 @ external hyp : ident -> constr := "ltac2" "hyp".
+(** Panics if there is more than one goal under focus. If there is no
+    goal under focus, looks for the section variable with the given name.
+    If there is one, looks for the hypothesis with the given name. *)
+
+(** Refinement *)
+
+Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine".