diff options
26 files changed, 239 insertions, 73 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e8ee0c537b..f26804e120 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -371,7 +371,7 @@ pkg:opam: - opam pin add --kind=path coqide.$COQ_VERSION . - set +e variables: - COQ_VERSION: "8.12" + COQ_VERSION: "8.13" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci diff --git a/META.coq.in b/META.coq.in index 377dbd9b7e..095f54dde7 100644 --- a/META.coq.in +++ b/META.coq.in @@ -1,7 +1,7 @@ # TODO: Generate automatically with Dune description = "The Coq Proof Assistant Plugin API" -version = "8.12" +version = "8.13" directory = "" requires = "" @@ -9,7 +9,7 @@ requires = "" package "config" ( description = "Coq Configuration Variables" - version = "8.12" + version = "8.13" directory = "config" @@ -19,7 +19,7 @@ package "config" ( package "clib" ( description = "Base General Coq Library" - version = "8.12" + version = "8.13" directory = "clib" requires = "str, unix, threads" @@ -31,7 +31,7 @@ package "clib" ( package "lib" ( description = "Base Coq-Specific Library" - version = "8.12" + version = "8.13" directory = "lib" @@ -45,7 +45,7 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.12" + version = "8.13" directory = "kernel/byterun" @@ -64,7 +64,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.12" + version = "8.13" directory = "kernel" @@ -78,7 +78,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.12" + version = "8.13" requires = "coq.kernel" @@ -92,7 +92,7 @@ package "library" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.12" + version = "8.13" requires = "coq.library" directory = "engine" @@ -105,7 +105,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.12" + version = "8.13" requires = "coq.engine" directory = "pretyping" @@ -118,7 +118,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.12" + version = "8.13" requires = "coq.pretyping" directory = "interp" @@ -131,7 +131,7 @@ package "interp" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.12" + version = "8.13" requires = "coq.interp" directory = "proofs" @@ -144,7 +144,7 @@ package "proofs" ( package "gramlib" ( description = "Coq Grammar Engine" - version = "8.12" + version = "8.13" requires = "coq.lib" directory = "gramlib/.pack" @@ -156,7 +156,7 @@ package "gramlib" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.12" + version = "8.13" requires = "coq.gramlib, coq.proofs" directory = "parsing" @@ -169,7 +169,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.12" + version = "8.13" requires = "coq.parsing" directory = "printing" @@ -182,7 +182,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.12" + version = "8.13" requires = "coq.printing" directory = "tactics" @@ -195,7 +195,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.12" + version = "8.13" requires = "coq.tactics" directory = "vernac" @@ -208,7 +208,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.12" + version = "8.13" requires = "coq.vernac" directory = "stm" @@ -221,7 +221,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.12" + version = "8.13" requires = "num, coq.stm" directory = "toplevel" @@ -234,7 +234,7 @@ package "toplevel" ( package "idetop" ( description = "Coq IDE Libraries" - version = "8.12" + version = "8.13" requires = "coq.toplevel" directory = "ide" @@ -247,7 +247,7 @@ package "idetop" ( package "ide" ( description = "Coq IDE Libraries" - version = "8.12" + version = "8.13" requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" @@ -260,7 +260,7 @@ package "ide" ( package "ideprotocol" ( description = "Coq IDE protocol" - version = "8.12" + version = "8.13" requires = "coq.toplevel" directory = "ide/protocol" @@ -273,14 +273,14 @@ package "ideprotocol" ( package "plugins" ( description = "Coq built-in plugins" - version = "8.12" + version = "8.13" directory = "plugins" package "ltac" ( description = "Coq LTAC Plugin" - version = "8.12" + version = "8.13" requires = "coq.stm" directory = "ltac" @@ -295,7 +295,7 @@ package "plugins" ( package "tauto" ( description = "Coq tauto plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "ltac" @@ -310,7 +310,7 @@ package "plugins" ( package "omega" ( description = "Coq omega plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "omega" @@ -325,7 +325,7 @@ package "plugins" ( package "micromega" ( description = "Coq micromega plugin" - version = "8.12" + version = "8.13" requires = "num,coq.plugins.ltac" directory = "micromega" @@ -340,7 +340,7 @@ package "plugins" ( package "zify" ( description = "Coq Zify plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "micromega" @@ -355,7 +355,7 @@ package "plugins" ( package "setoid_ring" ( description = "Coq newring plugin" - version = "8.12" + version = "8.13" requires = "" directory = "setoid_ring" @@ -370,7 +370,7 @@ package "plugins" ( package "extraction" ( description = "Coq extraction plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "extraction" @@ -385,7 +385,7 @@ package "plugins" ( package "cc" ( description = "Coq cc plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "cc" @@ -400,7 +400,7 @@ package "plugins" ( package "firstorder" ( description = "Coq ground plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "firstorder" @@ -415,7 +415,7 @@ package "plugins" ( package "rtauto" ( description = "Coq rtauto plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "rtauto" @@ -430,7 +430,7 @@ package "plugins" ( package "btauto" ( description = "Coq btauto plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "btauto" @@ -445,7 +445,7 @@ package "plugins" ( package "funind" ( description = "Coq recdef plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.extraction" directory = "funind" @@ -460,7 +460,7 @@ package "plugins" ( package "nsatz" ( description = "Coq nsatz plugin" - version = "8.12" + version = "8.13" requires = "num,coq.plugins.ltac" directory = "nsatz" @@ -475,7 +475,7 @@ package "plugins" ( package "rsyntax" ( description = "Coq rsyntax plugin" - version = "8.12" + version = "8.13" requires = "" directory = "syntax" @@ -490,7 +490,7 @@ package "plugins" ( package "int63syntax" ( description = "Coq int63syntax plugin" - version = "8.12" + version = "8.13" requires = "" directory = "syntax" @@ -505,7 +505,7 @@ package "plugins" ( package "string_notation" ( description = "Coq string_notation plugin" - version = "8.12" + version = "8.13" requires = "" directory = "syntax" @@ -520,7 +520,7 @@ package "plugins" ( package "derive" ( description = "Coq derive plugin" - version = "8.12" + version = "8.13" requires = "" directory = "derive" @@ -535,7 +535,7 @@ package "plugins" ( package "ssrmatching" ( description = "Coq ssrmatching plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "ssrmatching" @@ -550,7 +550,7 @@ package "plugins" ( package "ssreflect" ( description = "Coq ssreflect plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ssrmatching" directory = "ssr" @@ -565,7 +565,7 @@ package "plugins" ( package "ltac2" ( description = "Coq Ltac2 Plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "../user-contrib/Ltac2" diff --git a/configure.ml b/configure.ml index 75c11dab5f..9cfa9d409e 100644 --- a/configure.ml +++ b/configure.ml @@ -12,11 +12,11 @@ #load "str.cma" open Printf -let coq_version = "8.12+alpha" -let coq_macos_version = "8.11.90" (** "[...] should be a string comprised of +let coq_version = "8.13+alpha" +let coq_macos_version = "8.12.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 81191 -let state_magic = 581191 +let vo_magic = 81291 +let state_magic = 581291 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; diff --git a/default.nix b/default.nix index 841bccb129..6b0e396d23 100644 --- a/default.nix +++ b/default.nix @@ -29,7 +29,7 @@ , shell ? false # We don't use lib.inNixShell because that would also apply # when in a nix-shell of some package depending on this one. -, coq-version ? "8.12-git" +, coq-version ? "8.13-git" }: with pkgs; diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9498ab8bbb..ae4c6328b5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,5 @@ +## Changes between Coq 8.12 and Coq 8.13 + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting 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/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 1a02d6e65d..ab615d5f65 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -707,5 +707,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq810.v theories/Compat/Coq811.v theories/Compat/Coq812.v + theories/Compat/Coq813.v </dd> </dl> 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/printing/printer.ml b/printing/printer.ml index c2f73715f0..2ad9e268c2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -905,7 +905,7 @@ let pr_assumptionset env sigma s = let pr_axiom env ax typ = match ax with | Constant kn -> - safe_pr_constant env kn ++ safe_pr_ltype env sigma typ + hov 1 (safe_pr_constant env kn ++ cut() ++ safe_pr_ltype env sigma typ) | Positive m -> hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> @@ -917,17 +917,17 @@ let pr_assumptionset env sigma s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in + let var = pr_id id ++ spc() ++ str ": " ++ pr_ltype_env env sigma typ in (var :: v, a, o, tr) | Axiom (axiom, []) -> let ax = pr_axiom env axiom typ in (v, ax :: a, o, tr) | Axiom (axiom,l) -> let ax = pr_axiom env axiom typ ++ - cut() ++ + spc() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ Label.print lbl ++ - str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) + str "used in " ++ Label.print lbl ++ + str " to prove" ++ fnl() ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) | Opaque kn -> diff --git a/test-suite/Makefile b/test-suite/Makefile index 9935c4eed0..f0f838680e 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/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 190c34262f..ca4858d7a7 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,17 +7,17 @@ bli : Type Axioms: bli : Type Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Closed under the global context Closed under the global context Axioms: 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/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index c86548440b..97b4e39168 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq812. +Import Coq.Compat.Coq813. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index a1c1209db6..c06dd6e450 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..f408e95d2e --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 00f4747e3e..83010f2149 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v index ee4bac3542..f52b559f84 100644 --- a/theories/Compat/Coq812.v +++ b/theories/Compat/Coq812.v @@ -9,4 +9,6 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.12 *) + +Require Export Coq.Compat.Coq813. Set Firstorder Solver auto with *. diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v new file mode 100644 index 0000000000..92544c6ed9 --- /dev/null +++ b/theories/Compat/Coq813.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.13 *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index c7ad5edb1f..eb386ea3e8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -263,6 +263,7 @@ let get_native_name s = with _ -> "" let get_compat_file = function + | "8.13" -> "Coq.Compat.Coq813" | "8.12" -> "Coq.Compat.Coq812" | "8.11" -> "Coq.Compat.Coq811" | "8.10" -> "Coq.Compat.Coq810" 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 -> |