More notations for basic tactics.

2 files changed, 20 insertions, 4 deletions

diff --git a/tests/example2.v b/tests/example2.v
index 526cbc39f5..76f069a5ae 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -116,3 +116,10 @@ intros n m He He' He''.
 rewrite <- &He by Std.assumption ().
 Control.refine (fun () => &He'').
 Qed.
+
+Goal forall n (r := if true then n else 0), r = n.
+Proof.
+intros n r.
+hnf in r.
+split.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 4ce9fc0dbd..4bba9a7495 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -139,6 +139,18 @@ Ltac2 Notation "edestruct"
   use(thunk(opt(seq("using", constr, bindings)))) :=
   destruct0 true ic use.
 
+Ltac2 default_on_concl cl :=
+match cl with
+| None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
+| Some cl => cl
+end.
+
+Ltac2 Notation "red" cl(opt(clause)) :=
+  Std.red (default_on_concl cl).
+
+Ltac2 Notation "hnf" cl(opt(clause)) :=
+  Std.hnf (default_on_concl cl).
+
 Ltac2 rewrite0 ev rw cl tac :=
   let tac := match tac with
   | None => None
@@ -146,10 +158,7 @@ Ltac2 rewrite0 ev rw cl tac :=
     let ((_, tac)) := p in
     Some tac
   end in
-  let cl := match cl with
-  | None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
-  | Some cl => cl
-  end in
+  let cl := default_on_concl cl in
   Std.rewrite ev rw cl tac.
 
 Ltac2 Notation "rewrite"