From 940da8a791b8b1c704f28662fa2e6a8f3ddf040f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 Sep 2017 18:57:18 +0200
Subject: Adding quotations for the assert family of tactics.

---
 theories/Notations.v | 7 +++++++
 theories/Std.v       | 7 ++++++-
 2 files changed, 13 insertions(+), 1 deletion(-)

(limited to 'theories')

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".
-- 
cgit v1.2.3