Extending the Coq API in Ltac2.

1 files changed, 5 insertions, 0 deletions

diff --git a/Control.v b/Control.v
index a476513ede..6b3b360abb 100644
--- a/Control.v
+++ b/Control.v
@@ -28,6 +28,11 @@ 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".