From 152b259b7b587ea949dd856b24beaf56466f3f27 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 5 Dec 2016 16:32:26 +0100 Subject: Fixing a precedence issue in type parameters. --- Control.v | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 Control.v (limited to 'Control.v') diff --git a/Control.v b/Control.v new file mode 100644 index 0000000000..a476513ede --- /dev/null +++ b/Control.v @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '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". + +(** 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". -- cgit v1.2.3