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

2 files changed, 63 insertions, 0 deletions

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]
+).