Notations for a few reduction functions.

2 files changed, 52 insertions, 0 deletions

diff --git a/tests/example2.v b/tests/example2.v
index bfb1b07e7a..1856663953 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -123,3 +123,37 @@ intros n r.
 hnf in r.
 split.
 Qed.
+
+Goal 1 = 0 -> 0 = 0.
+Proof.
+intros H.
+pattern 0 at 1.
+let occ := 2 in pattern 1 at 1, 0 at $occ in H.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+native_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2 - 0 -> True.
+Proof.
+intros H.
+vm_compute plus in H.
+reflexivity.
+Qed.
+
+Goal 1 = 0 -> True /\ True.
+Proof.
+intros H.
+split; fold (1 + 0) (1 + 0) in H.
+reflexivity.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 910b6d5463..8c2c09a2b5 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -257,6 +257,24 @@ Ltac2 Notation "hnf" cl(opt(clause)) :=
   Std.hnf (default_on_concl cl).
 Ltac2 Notation hnf := hnf.
 
+Ltac2 Notation "vm_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause)) :=
+  Std.vm pl (default_on_concl cl).
+Ltac2 Notation vm_compute := vm_compute.
+
+Ltac2 Notation "native_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause)) :=
+  Std.native pl (default_on_concl cl).
+Ltac2 Notation native_compute := native_compute.
+
+Ltac2 fold0 pl cl :=
+  let cl := default_on_concl cl in
+  Control.enter (fun () => Control.with_holes pl (fun pl => Std.fold pl cl)).
+
+Ltac2 Notation "fold" pl(thunk(list1(open_constr))) cl(opt(clause)) :=
+  fold0 pl cl.
+
+Ltac2 Notation "pattern" pl(list1(seq(constr, occurrences), ",")) cl(opt(clause)) :=
+  Std.pattern pl (default_on_concl cl).
+
 Ltac2 rewrite0 ev rw cl tac :=
   let tac := match tac with
   | None => None