Add Ltac2 util and clean up old version cruft

.gitignore

@@ -94,6 +94,7 @@ src/Rewriter/Util/plugins/definition_by_tactic_plugin.ml
 src/Rewriter/Util/plugins/inductive_from_elim_plugin.ml
 src/Rewriter/Util/plugins/rewriter_build_plugin.ml
 src/Rewriter/Util/plugins/strategy_tactic_plugin.ml
+src/Rewriter/Util/plugins/ltac2_extra_plugin.ml
 
 src/Rewriter/Util/plugins/RewriterBuildRegistry.v
 src/Rewriter/Util/plugins/RewriterBuild.v
@@ -114,10 +115,10 @@ src/Rewriter/Util/plugins/strategy_tactic.ml
 src/Rewriter/Util/plugins/strategy_tactic.mli
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
-src/Rewriter/Util/plugins/definition_by_tactic_plugin.ml4
-src/Rewriter/Util/plugins/inductive_from_elim_plugin.ml4
-src/Rewriter/Util/plugins/rewriter_build_plugin.ml4
-src/Rewriter/Util/plugins/strategy_tactic_plugin.ml4
+src/Rewriter/Util/plugins/ltac2_extra.ml
+src/Rewriter/Util/plugins/ltac2_extra.mli
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
 
 /.coq-version
 /.coq-version-compilation-date

Makefile

@@ -37,17 +37,16 @@ $(COQ_VERSION_FILE)::
 endif
 
 _CoqProject: _CoqProject.in
-	sed 's/@ML4_OR_MLG@/$(ML4_OR_MLG)/g; s/@NATIVE_COMPILER_ARG@/$(NATIVE_COMPILER_ONDEMAND_COQPROJECT_FRAGMENT)/g ; s?@META@?$(META_FILE_FRAGMENT)?g' $< > $@
+	sed 's?@META@?$(META_FILE_FRAGMENT)?g' $< > $@
 
 # This target is used to update the _CoqProject file.
 # But it only works if we have git
 ifneq (,$(wildcard .git/))
 SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
 EXISTING_COQPROJECT_CONTENTS_SORTED:=$(shell cat _CoqProject.in 2>&1 | $(SORT_COQPROJECT))
-WARNINGS_PLUS := +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality
-# Remove unsupported-attributes once we stop supporting < 8.14
+WARNINGS_PLUS := +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field
 WARNINGS := $(WARNINGS_PLUS),unsupported-attributes
-COQPROJECT_CMD:=(echo @META@; echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-I $(PLUGINS_DIR)'; echo '-arg -w -arg $(WARNINGS)'; echo '@NATIVE_COMPILER_ARG@'; (git ls-files '$(SRC_DIR)/*.v' '$(SRC_DIR)/*.mlg' '$(SRC_DIR)/*.mllib' '$(SRC_DIR)/*.ml' '$(SRC_DIR)/*.mli' | $(SORT_COQPROJECT)); (echo '$(COMPATIBILITY_FILES_PATTERN)' | tr ' ' '\n'))
+COQPROJECT_CMD:=(echo @META@; echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-I $(PLUGINS_DIR)'; echo '-arg -w -arg $(WARNINGS)'; echo '-arg -native-compiler -arg ondemand'; (git ls-files '$(SRC_DIR)/*.v' '$(SRC_DIR)/*.mlg' '$(SRC_DIR)/*.mllib' '$(SRC_DIR)/*.ml' '$(SRC_DIR)/*.mli' | $(SORT_COQPROJECT)); (echo '$(COMPATIBILITY_FILES)' | tr ' ' '\n'))
 NEW_COQPROJECT_CONTENTS_SORTED:=$(shell $(COQPROJECT_CMD) | $(SORT_COQPROJECT))
 
 ifneq ($(EXISTING_COQPROJECT_CONTENTS_SORTED),$(NEW_COQPROJECT_CONTENTS_SORTED))

Makefile.local-late

@@ -11,8 +11,10 @@ $(COMPATIBILITY_FILES) : % : %$(EXPECTED_EXT) $(COQ_VERSION_FILE)
 # ensure that the ml compat files exist before we call coqdep on the corresponding .v files
 $(ALLDFILES): $(COMPATIBILITY_FILES) $(COQ_VERSION_FILE) _CoqProject
 
-# Remove -undeclared-scope once we stop supporting 8.9
-OTHERFLAGS += -w -notation-overridden,-undeclared-scope
+OTHERFLAGS += -w -notation-overridden
 ifneq ($(PROFILE),)
 OTHERFLAGS += -profile-ltac
 endif
+
+# Kludge around COQBUG(https://github.com/coq/coq/issues/16591)
+FINDLIBPKGS += -package coq-core.plugins.ltac2

Makefile.local.common

@@ -13,74 +13,44 @@ COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell $(COQBIN)coqc
 COQ_EXTENDED_VERSION := $(shell (echo | $(COQBIN)coqtop 2>/dev/null; $(COQBIN)coqc --version 2>/dev/null))
 COQ_EXTENDED_VERSION_OLD := $(shell cat $(COQ_VERSION_FILE) 2>/dev/null)
 
-ifneq (,$(filter 8.9%,$(COQ_VERSION)))
-EXPECTED_EXT:=.v89
-ML_DESCRIPTION := "Coq v8.9"
-ML4_OR_MLG := ml4
-NATIVE_COMPILER_ONDEMAND_COQPROJECT_FRAGMENT :=
-else
-ML4_OR_MLG := mlg
-NATIVE_COMPILER_ONDEMAND_COQPROJECT_FRAGMENT := -arg -native-compiler -arg ondemand
-ifneq (,$(filter 8.10%,$(COQ_VERSION)))
-EXPECTED_EXT:=.v810
-ML_DESCRIPTION := "Coq v8.10"
-else
-ifneq (,$(filter 8.11%,$(COQ_VERSION)))
-EXPECTED_EXT:=.v811
-ML_DESCRIPTION := "Coq v8.11"
-else
-ifneq (,$(filter 8.12%,$(COQ_VERSION)))
-EXPECTED_EXT:=.v812
-ML_DESCRIPTION := "Coq v8.12"
-else
-ifneq (,$(filter 8.13%,$(COQ_VERSION)))
-EXPECTED_EXT:=.v813
-ML_DESCRIPTION := "Coq v8.13"
-else
-ifneq (,$(filter 8.14%,$(COQ_VERSION)))
-EXPECTED_EXT:=.v814
-ML_DESCRIPTION := "Coq v8.14"
-else
 ifneq (,$(filter 8.15%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v815
 ML_DESCRIPTION := "Coq v8.15"
+META_FILE_FRAGMENT :=
 else
+META_FILE_FRAGMENT := src/Rewriter/Util/plugins/META.coq-rewriter
 ifneq (,$(filter 8.16%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v816
 ML_DESCRIPTION := "Coq v8.16"
-META_FILE_FRAGMENT := src/Rewriter/Util/plugins/META.coq-rewriter
 else
 EXPECTED_EXT:=.v817
 ML_DESCRIPTION := "Coq v8.17"
-META_FILE_FRAGMENT := src/Rewriter/Util/plugins/META.coq-rewriter
-endif
-endif
-endif
-endif
-endif
-endif
 endif
 endif
 
-COMPATIBILITY_FILES_PATTERN := \
+COMPATIBILITY_FILES := \
 	src/Rewriter/Util/plugins/definition_by_tactic.ml \
 	src/Rewriter/Util/plugins/definition_by_tactic.mli \
-	src/Rewriter/Util/plugins/definition_by_tactic_plugin.@ML4_OR_MLG@ \
+	src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg \
 	src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib \
 	src/Rewriter/Util/plugins/inductive_from_elim.ml \
 	src/Rewriter/Util/plugins/inductive_from_elim.mli \
-	src/Rewriter/Util/plugins/inductive_from_elim_plugin.@ML4_OR_MLG@ \
+	src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg \
 	src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib \
 	src/Rewriter/Util/plugins/rewriter_build.ml \
 	src/Rewriter/Util/plugins/rewriter_build.mli \
-	src/Rewriter/Util/plugins/rewriter_build_plugin.@ML4_OR_MLG@ \
+	src/Rewriter/Util/plugins/rewriter_build_plugin.mlg \
 	src/Rewriter/Util/plugins/rewriter_build_plugin.mllib \
 	src/Rewriter/Util/plugins/strategy_tactic.ml \
 	src/Rewriter/Util/plugins/strategy_tactic.mli \
-	src/Rewriter/Util/plugins/strategy_tactic_plugin.@ML4_OR_MLG@ \
+	src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg \
 	src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib \
+	src/Rewriter/Util/plugins/ltac2_extra.ml \
+	src/Rewriter/Util/plugins/ltac2_extra.mli \
+	src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg \
+	src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib \
 	src/Rewriter/Util/plugins/RewriterBuildRegistry.v \
+	src/Rewriter/Util/plugins/RewriterBuild.v \
 	src/Rewriter/Util/plugins/StrategyTactic.v \
-	src/Rewriter/Util/plugins/RewriterBuild.v
-
-COMPATIBILITY_FILES := $(subst @ML4_OR_MLG@,$(ML4_OR_MLG),$(COMPATIBILITY_FILES_PATTERN))
+	src/Rewriter/Util/plugins/Ltac2Extra.v \
+	#

_CoqProject.in

@@ -1,8 +1,8 @@
 @META@
 -R src/Rewriter Rewriter
 -I src/Rewriter/Util/plugins
--arg -w -arg +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes
-@NATIVE_COMPILER_ARG@
+-arg -w -arg +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field,unsupported-attributes
+-arg -native-compiler -arg ondemand
 src/Rewriter/Demo.v
 src/Rewriter/Language/IdentifiersBasicGenerate.v
 src/Rewriter/Language/IdentifiersBasicLibrary.v
@@ -110,6 +110,7 @@ src/Rewriter/Util/Tactics/WarnIfGoalsRemain.v
 src/Rewriter/Util/Tactics2/Array.v
 src/Rewriter/Util/Tactics2/Char.v
 src/Rewriter/Util/Tactics2/Constr.v
+src/Rewriter/Util/Tactics2/FixNotationsForPerformance.v
 src/Rewriter/Util/Tactics2/Head.v
 src/Rewriter/Util/Tactics2/HeadReference.v
 src/Rewriter/Util/Tactics2/Ident.v
@@ -126,20 +127,26 @@ src/Rewriter/Util/Tactics2/Constr/Unsafe/MakeAbbreviations.v
 src/Rewriter/Util/plugins/RewriterBuildRegistryImports.v
 src/Rewriter/Util/plugins/definition_by_tactic.ml
 src/Rewriter/Util/plugins/definition_by_tactic.mli
-src/Rewriter/Util/plugins/definition_by_tactic_plugin.@ML4_OR_MLG@
+src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg
 src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib
 src/Rewriter/Util/plugins/inductive_from_elim.ml
 src/Rewriter/Util/plugins/inductive_from_elim.mli
-src/Rewriter/Util/plugins/inductive_from_elim_plugin.@ML4_OR_MLG@
+src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg
 src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib
 src/Rewriter/Util/plugins/rewriter_build.ml
 src/Rewriter/Util/plugins/rewriter_build.mli
-src/Rewriter/Util/plugins/rewriter_build_plugin.@ML4_OR_MLG@
+src/Rewriter/Util/plugins/rewriter_build_plugin.mlg
 src/Rewriter/Util/plugins/rewriter_build_plugin.mllib
 src/Rewriter/Util/plugins/strategy_tactic.ml
 src/Rewriter/Util/plugins/strategy_tactic.mli
-src/Rewriter/Util/plugins/strategy_tactic_plugin.@ML4_OR_MLG@
+src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
+src/Rewriter/Util/plugins/ltac2_extra.ml
+src/Rewriter/Util/plugins/ltac2_extra.mli
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
 src/Rewriter/Util/plugins/RewriterBuildRegistry.v
-src/Rewriter/Util/plugins/StrategyTactic.v
 src/Rewriter/Util/plugins/RewriterBuild.v
+src/Rewriter/Util/plugins/StrategyTactic.v
+src/Rewriter/Util/plugins/Ltac2Extra.v
+

src/Rewriter/Language/Language.v

@@ -1530,22 +1530,40 @@ Module Compilers.
       {
         base_beq : base -> base -> bool;
         base_interp_beq : forall {t1 t2}, base_interp t1 -> base_interp t2 -> bool;
-        try_make_transport_base_cps :> type.try_make_transport_cpsT base;
-        baseHasNat :> base.type.BaseTypeHasNatT base;
-        buildIdent :> ident.BuildIdentT base_interp ident;
-        toRestrictedIdent :> ident.ToRestrictedIdentT ident;
-        buildEagerIdent :> ident.BuildEagerIdentT ident;
-        invertIdent :> InvertIdentT base_interp ident;
-        defaultBase :> @DefaultValue.type.base.DefaultT base base_interp;
-        reflect_base_beq :> reflect_rel (@eq base) base_beq;
-        reflect_base_interp_beq :> forall {t}, reflect_rel (@eq (base_interp t)) (@base_interp_beq t t);
-        try_make_transport_base_cps_correct :> type.try_make_transport_cps_correctT base;
-        baseHasNatCorrect :> base.BaseHasNatCorrectT base_interp;
-        toFromRestrictedIdent :> ident.ToFromRestrictedIdentT ident;
-        buildInvertIdentCorrect :> BuildInvertIdentCorrectT;
-        buildInterpIdentCorrect :> ident.BuildInterpIdentCorrectT ident_interp;
-        buildInterpEagerIdentCorrect :> ident.BuildInterpEagerIdentCorrectT ident_interp;
-        ident_interp_Proper :> forall t, Proper (eq ==> type.eqv) (ident_interp t)
+        try_make_transport_base_cps : type.try_make_transport_cpsT base;
+        baseHasNat : base.type.BaseTypeHasNatT base;
+        buildIdent : ident.BuildIdentT base_interp ident;
+        toRestrictedIdent : ident.ToRestrictedIdentT ident;
+        buildEagerIdent : ident.BuildEagerIdentT ident;
+        invertIdent : InvertIdentT base_interp ident;
+        defaultBase : @DefaultValue.type.base.DefaultT base base_interp;
+        reflect_base_beq : reflect_rel (@eq base) base_beq;
+        reflect_base_interp_beq : forall {t}, reflect_rel (@eq (base_interp t)) (@base_interp_beq t t);
+        try_make_transport_base_cps_correct : type.try_make_transport_cps_correctT base;
+        baseHasNatCorrect : base.BaseHasNatCorrectT base_interp;
+        toFromRestrictedIdent : ident.ToFromRestrictedIdentT ident;
+        buildInvertIdentCorrect : BuildInvertIdentCorrectT;
+        buildInterpIdentCorrect : ident.BuildInterpIdentCorrectT ident_interp;
+        buildInterpEagerIdentCorrect : ident.BuildInterpEagerIdentCorrectT ident_interp;
+        ident_interp_Proper : forall t, Proper (eq ==> type.eqv) (ident_interp t)
       }.
+    #[global]
+     Existing Instances
+     try_make_transport_base_cps
+     baseHasNat
+     buildIdent
+     toRestrictedIdent
+     buildEagerIdent
+     invertIdent
+     defaultBase
+     reflect_base_beq
+     reflect_base_interp_beq
+     try_make_transport_base_cps_correct
+     baseHasNatCorrect
+     toFromRestrictedIdent
+     buildInvertIdentCorrect
+     buildInterpIdentCorrect
+     buildInterpEagerIdentCorrect
+     ident_interp_Proper.
   End Classes.
 End Compilers.

src/Rewriter/Language/Pre.v

@@ -81,6 +81,7 @@ Module RewriteRuleNotations.
         | ls' => ltac:(mymap_do_again ls')
         end) (only parsing).
 
+  Declare Scope rew_rules_scope.
   Delimit Scope rew_rules_scope with rew_rules.
   Notation "x ++ y"
     := (match x%rew_rules, y%rew_rules return _ with

src/Rewriter/Language/UnderLets.v

@@ -116,6 +116,7 @@ Module Compilers.
     End with_var.
     Module Export Notations.
       Global Arguments UnderLets : clear implicits.
+      Declare Scope under_lets_scope.
       Delimit Scope under_lets_scope with under_lets.
       Bind Scope under_lets_scope with UnderLets.UnderLets.
       Notation "x <-- y ; f" := (UnderLets.splice y (fun x => f%under_lets)) : under_lets_scope.

src/Rewriter/Rewriter/Rewriter.v

@@ -339,6 +339,7 @@ Module Compilers.
     | App {s d} (f : pattern (s -> d)) (x : pattern s) : pattern d.
 
     Module Export Notations.
+      Declare Scope pattern_scope.
       Delimit Scope pattern_scope with pattern.
       Bind Scope pattern_scope with pattern.
       Infix "@" := App : pattern_scope.

src/Rewriter/Util/CPSNotations.v

@@ -4,6 +4,7 @@ Local Set Universe Polymorphism.
 (** [x <- f ; C] encodes a call to function [f] with [C] as the
   continuation. In [C], [x] refers to the output of [f]. *)
 
+Declare Scope cps_scope.
 Delimit Scope cps_scope with cps.
 
 (* [cpscall] is a marker to get Coq to print code using this notation only when it was actually used *)

src/Rewriter/Util/InductiveHList.v

@@ -15,6 +15,7 @@ Fixpoint nth (n : nat) (l : hlist) {T} (default : T) {struct l} : nth_type n l T
   end.
 
 Module Export Notations.
+  Declare Scope hlist_scope.
   Delimit Scope hlist_scope with hlist.
   Bind Scope hlist_scope with hlist.
   Notation "[ ]" := nil (format "[ ]") : hlist_scope.

src/Rewriter/Util/Option.v

@@ -76,6 +76,7 @@ Notation value := sequence_return (only parsing).
 Notation get_default := sequence_return (only parsing).
 
 Module Export Notations.
+  Declare Scope option_scope.
   Delimit Scope option_scope with option.
   Bind Scope option_scope with option.
 

src/Rewriter/Util/PrimitiveProd.v

@@ -12,6 +12,8 @@ Require Import Rewriter.Util.GlobalSettings.
 
 Local Set Primitive Projections.
 
+Declare Scope primproj_type_scope.
+Declare Scope primproj_scope.
 Delimit Scope primproj_type_scope with primproj_type.
 Delimit Scope primproj_scope with primproj.
 

src/Rewriter/Util/PrimitiveSigma.v

@@ -13,6 +13,8 @@ Require Import Rewriter.Util.Notations.
 
 Local Set Primitive Projections.
 
+Declare Scope primproj_type_scope.
+Declare Scope primproj_scope.
 Delimit Scope primproj_type_scope with primproj_type.
 Delimit Scope primproj_scope with primproj.
 

src/Rewriter/Util/Strings/Parse/Common.v

@@ -9,6 +9,7 @@ Local Open Scope char_scope.
 Local Open Scope string_scope.
 
 Definition ParserAction T := string -> list (T * string).
+Declare Scope parse_scope.
 Delimit Scope parse_scope with parse.
 Bind Scope parse_scope with ParserAction.
 Definition parse_impossible {T} : ParserAction T

src/Rewriter/Util/Strings/ParseArithmetic.v

@@ -114,6 +114,7 @@ Redirect "log" Check let ls := [("-1234", -(1234):Q); ("0xF", 15:Q); ("10.5", (1
 
 Inductive Qexpr := Qv (_ : Q) | Qeopp (a : Qexpr) | Qeadd (a b : Qexpr) | Qesub (a b : Qexpr) | Qemul (a b : Qexpr) | Qediv (a b : Qexpr) | Qepow (b e : Qexpr).
 Coercion Qv : Q >-> Qexpr.
+Declare Scope Qexpr_scope.
 Delimit Scope Qexpr_scope with Qexpr.
 Bind Scope Qexpr_scope with Qexpr.
 Infix "^" := Qepow : Qexpr_scope.

src/Rewriter/Util/Tactics2/FixNotationsForPerformance.v

@@ -0,0 +1,42 @@
+Require Import Ltac2.Ltac2.
+Require Export Ltac2.Notations.
+Require Export Rewriter.Util.FixCoqMistakes.
+
+(** We replace notations taking constr with tactic, so that we don't
+    pay the cost of retyping, see
+    COQBUG(https://github.com/coq/coq/issues/16586) *)
+
+(** Base tactics *)
+
+Ltac2 Notation "eval" "red" "in" c(tactic(6)) :=
+  Std.eval_red c.
+
+Ltac2 Notation "eval" "hnf" "in" c(tactic(6)) :=
+  Std.eval_hnf c.
+
+Ltac2 Notation "eval" "simpl" s(strategy) pl(opt(seq(pattern, occurrences))) "in" c(tactic(6)) :=
+  Std.eval_simpl s pl c.
+
+Ltac2 Notation "eval" "cbv" s(strategy) "in" c(tactic(6)) :=
+  Std.eval_cbv s c.
+
+Ltac2 Notation "eval" "cbn" s(strategy) "in" c(tactic(6)) :=
+  Std.eval_cbn s c.
+
+Ltac2 Notation "eval" "lazy" s(strategy) "in" c(tactic(6)) :=
+  Std.eval_lazy s c.
+
+Ltac2 Notation "eval" "unfold" pl(list1(seq(reference, occurrences), ",")) "in" c(tactic(6)) :=
+  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(tactic(2), occurrences), ",")) "in" c(tactic(6)) :=
+  Std.eval_pattern pl c.
+
+Ltac2 Notation "eval" "vm_compute" pl(opt(seq(pattern, occurrences))) "in" c(tactic(6)) :=
+  Std.eval_vm pl c.
+
+Ltac2 Notation "eval" "native_compute" pl(opt(seq(pattern, occurrences))) "in" c(tactic(6)) :=
+  Std.eval_native pl c.

src/Rewriter/Util/Tactics2/Notations.v

@@ -2,3 +2,4 @@ Require Import Ltac2.Ltac2.
 Require Export Rewriter.Util.FixCoqMistakes.
 
 Ltac2 Notation "strategy:(" s(strategy) ")" := s.
+Ltac2 Notation "occurrences:(" o(occurrences) ")" := o.

src/Rewriter/Util/TypeList.v

@@ -8,6 +8,7 @@ Fixpoint nth (n : nat) (l : t) (default : Type) {struct l} :=
   end.
 
 Module Export Notations.
+  Declare Scope type_list_scope.
   Delimit Scope type_list_scope with type_list.
   Bind Scope type_list_scope with t.
   Notation "[ ]" := nil (format "[ ]") : type_list_scope.