diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 7 | ||||
| -rw-r--r-- | theories/Std.v | 7 |
2 files changed, 13 insertions, 1 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index d4520dbdfd..91025ea964 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -279,6 +279,13 @@ Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) := Ltac2 Notation "eset" p(thunk(pose)) cl(opt(clause)) := Std.set true p (default_on_concl cl). +Ltac2 assert0 ev ast := + enter_h ev (fun _ ast => Std.assert ast) ast. + +Ltac2 Notation "assert" ast(thunk(assert)) := assert0 false ast. + +Ltac2 Notation "eassert" ast(thunk(assert)) := assert0 true ast. + Ltac2 default_everywhere cl := match cl with | None => { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences } diff --git a/theories/Std.v b/theories/Std.v index 2eab172432..7831baf046 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -88,6 +88,11 @@ Ltac2 Type induction_clause := { indcl_in : clause option; }. +Ltac2 Type assertion := [ +| AssertType (intro_pattern option, constr, (unit -> unit) option) +| AssertValue (ident, constr) +]. + Ltac2 Type repeat := [ | Precisely (int) | UpTo (int) @@ -131,7 +136,7 @@ Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "ltac2" "ta Ltac2 @ external generalize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_generalize". -Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_assert". +Ltac2 @ external assert : assertion -> unit := "ltac2" "tac_assert". Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough". Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose". |