Ltac2: add notations for eval cbv in ... and other in place reductions

3 files changed, 71 insertions, 0 deletions

diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v
index 3d2a875e38..32c8a7cbe7 100644
--- a/test-suite/ltac2/notations.v
+++ b/test-suite/ltac2/notations.v
@@ -1,6 +1,8 @@
 From Ltac2 Require Import Ltac2.
 From Coq Require Import ZArith String List.
 
+(** * Test cases for the notation system itself *)
+
 Open Scope Z_scope.
 
 Check 1 + 1 : Z.
@@ -22,3 +24,9 @@ Lemma maybe : list bool.
 Proof.
   refine (sl ["left" =? "right"]).
 Qed.
+
+(** * Test cases for specific notations with special contexts *)
+
+(** ** Test eval ... in / reduction tactics *)
+
+(** Moved to test-suite/output/ltac2_notations_eval_in.v so that the output can be checked s*)
diff --git a/test-suite/output/ltac2_notations_eval_in.out b/test-suite/output/ltac2_notations_eval_in.out
new file mode 100644
index 0000000000..15e43b7fb9
--- /dev/null
+++ b/test-suite/output/ltac2_notations_eval_in.out
@@ -0,0 +1,21 @@
+- : constr =
+constr:((fix add (n m : nat) {struct n} : nat :=
+           match n with
+           | 0 => m
+           | S p => S (add p m)
+           end) (1 + 2) 3)
+- : constr = constr:(S (0 + 2 + 3))
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr list = [constr:(0 <> 0); constr:(0 = 0 -> False);
+constr:((fun P : Prop => P -> False) (0 = 0)); constr:(
+0 <> 0)]
diff --git a/test-suite/output/ltac2_notations_eval_in.v b/test-suite/output/ltac2_notations_eval_in.v
new file mode 100644
index 0000000000..4a11e7cae0
--- /dev/null
+++ b/test-suite/output/ltac2_notations_eval_in.v
@@ -0,0 +1,42 @@
+From Ltac2 Require Import Ltac2.
+From Coq Require Import ZArith.
+
+(** * Test eval ... in / reduction tactics *)
+
+(** The below test cases test if the notation syntax works - not the tactics as such *)
+
+Ltac2 Eval (eval red in (1+2+3)).
+
+Ltac2 Eval (eval hnf in (1+2+3)).
+
+Ltac2 Eval (eval simpl in (1+2+3)).
+
+Ltac2 Eval (eval simpl Z.add in (1+2+3)).
+
+Ltac2 Eval (eval cbv in (1+2+3)).
+
+Ltac2 Eval (eval cbv delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbv delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbn in (1+2+3)).
+
+Ltac2 Eval (eval cbn delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbn delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval lazy in (1+2+3)).
+
+Ltac2 Eval (eval lazy delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval lazy delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+(* The example for [fold] in the reference manual *)
+
+Ltac2 Eval (
+  let t1 := '(~0=0) in
+  let t2 := eval unfold not in $t1 in
+  let t3 := eval pattern (0=0) in $t2 in
+  let t4 := eval fold not in $t3 in
+  [t1; t2; t3; t4]
+).