From e6b295a62a82df6fa92b559bb3ce079d5fa42240 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Wed, 1 Apr 2020 16:38:17 +0200
Subject: Ltac2: add notations for eval cbv in ... and other in place
 reductions

---
 user-contrib/Ltac2/Notations.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 390b39bab1..931d753521 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -396,6 +396,39 @@ 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 Notation "eval" "red" "in" c(constr) :=
+  Std.eval_red c.
+
+Ltac2 Notation "eval" "hnf" "in" c(constr) :=
+  Std.eval_hnf c.
+
+Ltac2 Notation "eval" "simpl" s(strategy) pl(opt(seq(pattern, occurrences))) "in" c(constr) :=
+  Std.eval_simpl s pl c.
+
+Ltac2 Notation "eval" "cbv" s(strategy) "in" c(constr) :=
+  Std.eval_cbv s c.
+
+Ltac2 Notation "eval" "cbn" s(strategy) "in" c(constr) :=
+  Std.eval_cbn s c.
+
+Ltac2 Notation "eval" "lazy" s(strategy) "in" c(constr) :=
+  Std.eval_lazy s c.
+
+Ltac2 Notation "eval" "unfold" pl(list1(seq(reference, occurrences), ",")) "in" c(constr) :=
+  Std.eval_unfold pl c.
+
+Ltac2 Notation "eval" "fold" pl(thunk(list1(open_constr))) "in" c(constr) :=
+  Std.eval_fold (pl ()) c.
+
+Ltac2 Notation "eval" "pattern" pl(list1(seq(constr, occurrences), ",")) "in" c(constr) :=
+  Std.eval_pattern pl c.
+
+Ltac2 Notation "eval" "vm_compute" pl(opt(seq(pattern, occurrences))) "in" c(constr) :=
+  Std.eval_vm pl c.
+
+Ltac2 Notation "eval" "native_compute" pl(opt(seq(pattern, occurrences))) "in" c(constr) :=
+  Std.eval_native pl c.
+
 Ltac2 change0 p cl :=
   let (pat, c) := p in
   Std.change pat c (default_on_concl cl).
-- 
cgit v1.2.3