aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst4
-rw-r--r--plugins/ssr/ssrvernac.mlg29
-rw-r--r--plugins/ssr/ssrvernac.mli2
-rw-r--r--plugins/ssrsearch/g_search.mlg4
-rw-r--r--test-suite/Makefile5
-rw-r--r--test-suite/ltac2/notations.v8
-rw-r--r--test-suite/output/ltac2_notations_eval_in.out21
-rw-r--r--test-suite/output/ltac2_notations_eval_in.v42
-rw-r--r--user-contrib/Ltac2/Notations.v33
-rw-r--r--vernac/g_vernac.mlg5
10 files changed, 148 insertions, 5 deletions
diff --git a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
new file mode 100644
index 0000000000..2f8d92fae5
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term`
+ (`#11981 <https://github.com/coq/coq/pull/11981>`_,
+ by Michael Soegtrop).
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 7ef3e44848..24772a8514 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -300,6 +300,35 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
Ssrview.AdaptorDb.declare k hints }
END
+(** Search compatibility *)
+
+{
+
+ let warn_search_moved_enabled = ref true
+ let warn_search_moved = CWarnings.create ~name:"ssr-search-moved"
+ ~category:"deprecated" ~default:CWarnings.Enabled
+ (fun () ->
+ (Pp.strbrk
+ "SSReflect's Search command has been moved to the \
+ ssrsearch module; please Require that module if you \
+ still want to use SSReflect's Search command"))
+
+open G_vernac
+}
+
+GRAMMAR EXTEND Gram
+ GLOBAL: query_command;
+
+ query_command:
+ [ [ IDENT "Search"; s = search_query; l = search_queries; "." ->
+ { let (sl,m) = l in
+ if !warn_search_moved_enabled then warn_search_moved ();
+ fun g ->
+ Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) }
+ ] ]
+;
+END
+
(** Keyword compatibility fixes. *)
(* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli
index 327a2d4660..93339313f0 100644
--- a/plugins/ssr/ssrvernac.mli
+++ b/plugins/ssr/ssrvernac.mli
@@ -9,3 +9,5 @@
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+
+val warn_search_moved_enabled : bool ref
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 1651e1cc71..6d68cc13ab 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -299,6 +299,10 @@ let ssrdisplaysearch gr env t =
let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
Feedback.msg_notice (hov 2 pr_res ++ fnl ())
+(* Remove the warning entirely when this plugin is loaded. *)
+let _ =
+ Ssreflect_plugin.Ssrvernac.warn_search_moved_enabled := false
+
let deprecated_search =
CWarnings.create
~name:"deprecated-ssr-search"
diff --git a/test-suite/Makefile b/test-suite/Makefile
index dece21885c..bbd31486fe 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -117,10 +117,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
# All subsystems
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
-PREREQUISITELOG = prerequisite/admit.v.log \
- prerequisite/make_local.v.log prerequisite/make_notation.v.log \
- prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \
- prerequisite/module_bug7192.v.log
+PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v))
#######################################################################
# Phony targets
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]
+).
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).
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index fe3bb9b890..45bf61d79e 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -35,6 +35,9 @@ open Attributes
let query_command = Entry.create "vernac:query_command"
+let search_query = Entry.create "vernac:search_query"
+let search_queries = Entry.create "vernac:search_queries"
+
let subprf = Entry.create "vernac:subprf"
let quoted_attributes = Entry.create "vernac:quoted_attributes"
@@ -819,7 +822,7 @@ GRAMMAR EXTEND Gram
END
GRAMMAR EXTEND Gram
- GLOBAL: command query_command class_rawexpr gallina_ext;
+ GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries;
gallina_ext:
[ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 02:42:51 +0000