From 3d60180c531d34f5312f790761fa7c9394a15e72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 29 Nov 2024 13:40:06 +0100 Subject: [PATCH] rename package coq-core -> rocq-runtime --- .github/workflows/ci-macos.yml | 4 +- .gitlab-ci.yml | 5 +- INSTALL.md | 4 +- Makefile | 22 +-- boot/dune | 8 +- boot/env.ml | 6 +- boot/env.mli | 4 +- checker/dune | 12 +- clib/dune | 6 +- config/dune | 12 +- coq-core.opam | 36 +--- coqide-server.opam | 2 +- coqpp/dune | 2 +- default.nix | 4 +- dev/bench/bench.sh | 5 +- dev/bench/dune | 2 +- dev/ci/ci-common.sh | 2 +- dev/ci/platform/coq-pf-03-build.bat | 1 + dev/doc/build-system.dune.md | 8 +- dev/doc/release-process.md | 2 +- dev/dune | 54 +++--- dev/dune-dbg.in | 4 +- dev/shim/dune | 48 +++--- dev/tools/coqdev.el | 2 +- doc/corelib/Library.tex | 2 +- doc/corelib/dune | 1 + doc/dune | 3 + doc/plugin_tutorial/dune | 2 +- .../tuto0/src/META.coq-plugin-tutorial | 2 +- doc/plugin_tutorial/tuto0/src/dune | 4 +- .../tuto1/src/META.coq-plugin-tutorial | 2 +- doc/plugin_tutorial/tuto1/src/dune | 4 +- .../tuto2/src/META.coq-plugin-tutorial | 2 +- doc/plugin_tutorial/tuto2/src/dune | 4 +- .../tuto3/src/META.coq-plugin-tutorial | 2 +- doc/plugin_tutorial/tuto3/src/dune | 4 +- doc/sphinx/practical-tools/utilities.rst | 4 +- .../proof-engine/vernacular-commands.rst | 6 +- doc/tools/docgram/dune | 2 +- dune | 8 +- dune-project | 14 +- engine/dune | 6 +- gramlib/dune | 8 +- ide/coqide/dune | 4 +- ide/coqide/protocol/dune | 2 +- index.mld | 4 +- interp/dune | 6 +- kernel/byterun/dune | 6 +- kernel/dune | 10 +- lib/cWarnings.mli | 2 +- lib/dune | 8 +- library/dune | 7 +- parsing/dune | 8 +- perf/dune | 6 +- plugins/btauto/dune | 8 +- plugins/btauto/g_btauto.mlg | 2 +- plugins/cc/dune | 16 +- plugins/cc/g_congruence.mlg | 2 +- plugins/derive/dune | 8 +- plugins/derive/g_derive.mlg | 4 +- plugins/extraction/dune | 8 +- plugins/extraction/g_extraction.mlg | 2 +- plugins/firstorder/dune | 16 +- plugins/firstorder/g_ground.mlg | 4 +- plugins/funind/dune | 8 +- plugins/funind/g_indfun.mlg | 2 +- plugins/ltac/coretactics.mlg | 8 +- plugins/ltac/dune | 16 +- plugins/ltac/extraargs.mlg | 6 +- plugins/ltac/extratactics.mlg | 2 +- plugins/ltac/g_auto.mlg | 2 +- plugins/ltac/g_class.mlg | 2 +- plugins/ltac/g_eqdecide.mlg | 2 +- plugins/ltac/g_ltac.mlg | 2 +- plugins/ltac/g_obligations.mlg | 2 +- plugins/ltac/g_rewrite.mlg | 2 +- plugins/ltac/g_tactic.mlg | 2 +- plugins/ltac/profile_ltac_tactics.mlg | 2 +- plugins/ltac/tauto.ml | 2 +- plugins/ltac2/dune | 8 +- plugins/ltac2/g_ltac2.mlg | 4 +- plugins/ltac2/tac2core.ml | 2 +- plugins/ltac2/tac2entries.ml | 4 +- plugins/ltac2/tac2stdlib.ml | 2 +- plugins/ltac2_ltac1/dune | 6 +- plugins/ltac2_ltac1/g_ltac2_ltac1.mlg | 2 +- plugins/ltac2_ltac1/tac2core_ltac1.ml | 2 +- plugins/ltac2_ltac1/tac2stdlib_ltac1.ml | 2 +- plugins/micromega/dune | 28 ++- plugins/micromega/g_micromega.mlg | 2 +- plugins/micromega/g_zify.mlg | 2 +- plugins/nsatz/dune | 16 +- plugins/nsatz/g_nsatz.mlg | 2 +- plugins/ring/dune | 8 +- plugins/ring/g_ring.mlg | 2 +- plugins/ring/ring.ml | 4 +- plugins/rtauto/dune | 8 +- plugins/rtauto/g_rtauto.mlg | 2 +- plugins/ssr/dune | 8 +- plugins/ssr/ssrparser.mlg | 10 +- plugins/ssr/ssrtacs.mlg | 6 +- plugins/ssr/ssrvernac.mlg | 6 +- plugins/ssrmatching/dune | 8 +- plugins/ssrmatching/g_ssrmatching.mlg | 6 +- plugins/ssrmatching/ssrmatching.ml | 4 +- plugins/syntax/dune | 8 +- plugins/syntax/g_number_string.mlg | 2 +- pretyping/dune | 6 +- printing/dune | 6 +- proofs/dune | 6 +- rocq-core.opam | 4 +- rocq-core.opam.template | 2 +- rocq-runtime.opam | 60 +++++++ ...pam.template => rocq-runtime.opam.template | 0 stdlib/dune-project | 2 +- stdlib/test-suite/micromega/witness_tactics.v | 2 +- stdlib/theories/btauto/Btauto.v | 2 +- stdlib/theories/funind/FunInd.v | 2 +- stdlib/theories/micromega/Lia.v | 4 +- stdlib/theories/micromega/Lqa.v | 4 +- stdlib/theories/micromega/Lra.v | 2 +- stdlib/theories/micromega/Psatz.v | 2 +- stdlib/theories/micromega/Zify.v | 2 +- stdlib/theories/micromega/ZifyInst.v | 2 +- stdlib/theories/nsatz/NsatzTactic.v | 4 +- stdlib/theories/rtauto/Rtauto.v | 2 +- stdlib/theories/setoid_ring/Ring_base.v | 2 +- stdlib/theories/setoid_ring/Ring_tac.v | 2 +- stm/asyncTaskQueue.ml | 2 +- stm/dune | 6 +- stm/stm.ml | 2 +- sysinit/dune | 18 +- tactics/dune | 6 +- test-suite/Makefile | 2 +- test-suite/bugs/bug_17069_1.v | 14 +- test-suite/bugs/bug_17687.v | 2 +- test-suite/bugs/bug_3612.v | 2 +- test-suite/bugs/bug_3649.v | 2 +- test-suite/bugs/bug_4121.v | 2 +- .../findlib-package-unpacked/run.sh | 2 +- .../coq-makefile/findlib-package/run.sh | 2 +- .../template/src/META.coq-test-suite | 2 +- test-suite/dune | 1 + test-suite/misc/coq_environment.sh | 2 +- .../src/META.coq-test-suite | 4 +- .../poly-capture-global-univs/src/evil.mlg | 2 +- .../misc/quotation_token/META.coq-test-suite | 2 +- .../misc/side-eff-leak-univs/src/evil.mlg | 2 +- test-suite/output/bug_17155.out | 2 +- test-suite/output/ltac2_anomaly_backtrace.out | 2 +- test-suite/output/ltac2_bt.out | 16 +- test-suite/output/ltac2_deprecated.v | 2 +- test-suite/output/ltac2_printabout.out | 2 +- test-suite/output/ltac2_printabout.v | 2 +- .../no-output-sync/time-of-build.log.in | 2 +- .../precomputed-time-tests/template/init.sh | 2 +- test-suite/prerequisite/funind.v | 2 +- test-suite/stm/classify_set_proof_mode_9093.v | 2 +- test-suite/success/Discriminate_HoTT.v | 2 +- test-suite/tools/dune | 2 +- theories/Init/Byte.v | 2 +- theories/Init/Ltac.v | 2 +- theories/Init/Prelude.v | 8 +- theories/Init/Tauto.v | 2 +- theories/derive/Derive.v | 2 +- theories/dune.disabled | 28 +-- theories/extraction/Extraction.v | 2 +- theories/ssr/ssreflect.v | 2 +- theories/ssrmatching/ssrmatching.v | 2 +- tools/CoqMakefile.in | 2 +- tools/coq_makefile.ml | 2 +- tools/coqdep/dune | 2 +- tools/coqdep/lib/dune | 8 +- tools/coqdep/lib/fl.ml | 2 +- tools/coqdoc/{main.ml => coqdoc.ml} | 0 tools/coqdoc/{main.mli => coqdoc.mli} | 0 tools/coqdoc/dune | 10 +- tools/coqworkmgr/dune | 8 +- tools/dune | 14 +- tools/dune_rule_gen/coq_rules.ml | 4 +- tools/dune_rule_gen/coq_rules.mli | 2 +- tools/dune_rule_gen/dune | 2 +- topbin/coqc_bin.ml | 2 +- topbin/dune | 24 +-- topbin/rocq.ml | 2 +- toplevel/dune | 8 +- user-contrib/Ltac2/Array.v | 16 +- user-contrib/Ltac2/Char.v | 4 +- user-contrib/Ltac2/Constant.v | 2 +- user-contrib/Ltac2/Constr.v | 64 +++---- user-contrib/Ltac2/Constructor.v | 6 +- user-contrib/Ltac2/Control.v | 60 +++---- user-contrib/Ltac2/Env.v | 8 +- user-contrib/Ltac2/Evar.v | 2 +- user-contrib/Ltac2/FMap.v | 22 +-- user-contrib/Ltac2/FSet.v | 36 ++-- user-contrib/Ltac2/Float.v | 2 +- user-contrib/Ltac2/Fresh.v | 8 +- user-contrib/Ltac2/Ident.v | 6 +- user-contrib/Ltac2/Ind.v | 18 +- user-contrib/Ltac2/Init.v | 4 +- user-contrib/Ltac2/Int.v | 32 ++-- user-contrib/Ltac2/Ltac1.v | 34 ++-- user-contrib/Ltac2/Message.v | 48 +++--- user-contrib/Ltac2/Meta.v | 2 +- user-contrib/Ltac2/Pattern.v | 14 +- user-contrib/Ltac2/Proj.v | 14 +- user-contrib/Ltac2/Pstring.v | 20 +-- user-contrib/Ltac2/Std.v | 160 +++++++++--------- user-contrib/Ltac2/String.v | 18 +- user-contrib/Ltac2/TransparentState.v | 6 +- user-contrib/Ltac2/Uint63.v | 8 +- user-contrib/Ltac2/Unification.v | 2 +- user-contrib/Ltac2/dune.disabled | 4 +- vernac/dune | 6 +- vernac/mltop.mli | 2 +- vernac/vernacextend.mli | 2 +- 217 files changed, 962 insertions(+), 735 deletions(-) create mode 100644 rocq-runtime.opam rename coq-core.opam.template => rocq-runtime.opam.template (100%) rename tools/coqdoc/{main.ml => coqdoc.ml} (100%) rename tools/coqdoc/{main.mli => coqdoc.mli} (100%) diff --git a/.github/workflows/ci-macos.yml b/.github/workflows/ci-macos.yml index 770819747d9e..728de341ad53 100644 --- a/.github/workflows/ci-macos.yml +++ b/.github/workflows/ci-macos.yml @@ -36,7 +36,7 @@ jobs: eval $(opam env) ./configure -prefix "$(pwd)/_install_ci" -native-compiler no make dunestrap - dune build -p coq-core,rocq-core,coqide-server,coqide + dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,coqide env: MACOSX_DEPLOYMENT_TARGET: "10.11" NJOBS: "2" @@ -44,7 +44,7 @@ jobs: - name: Install Coq run: | eval $(opam env) - dune install --prefix="$(pwd)/_install_ci" coq-core rocq-core coqide-server coqide + dune install --prefix="$(pwd)/_install_ci" rocq-runtime coq-core rocq-core coqide-server coqide - name: Run Coq Test Suite run: | diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ae2b9e9ce722..9124481c8ce8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -81,7 +81,7 @@ before_script: - config/dune.c_flags expire_in: 1 week script: - - PKGS=coq-core,rocq-core,coqide-server + - PKGS=rocq-runtime,coq-core,rocq-core,coqide-server - if [ "$COQIDE" != "no" ]; then PKGS=${PKGS},coqide; fi - dev/ci/gitlab-section.sh start coq.clean coq.clean - make clean # ensure that `make clean` works on a fresh clone @@ -232,6 +232,7 @@ before_script: # OPAM will build out-of-tree so no point in importing artifacts script: - if [ "$COQ_CI_NATIVE" = true ]; then opam install -y coq-native; fi + - opam pin add --kind=path rocq-runtime.dev . - opam pin add --kind=path coq-core.dev . - opam pin add --kind=path rocq-core.dev . - opam pin add --kind=path coq-stdlib.dev stdlib/ @@ -336,7 +337,7 @@ build:base:dev:dune: script: - cp theories/dune.disabled theories/dune - cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune - - dune build -p coq-core,rocq-core,coqide-server + - dune build -p rocq-runtime,coq-core,rocq-core,coqide-server - ls _build/install/default/lib/coq/theories/Init/Prelude.vo - ls _build/install/default/lib/coq/user-contrib/Ltac2/Ltac2.vo only: *full-ci diff --git a/INSTALL.md b/INSTALL.md index 5b4cd755b545..5dff951087b1 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -91,8 +91,8 @@ To build and install Coq (and CoqIDE if desired) do: $ ./configure -prefix $options $ make dunestrap - $ dune build -p coq-core,rocq-core,coq,coqide-server,coqide - $ dune install --prefix= coq-core rocq-core coq coqide-server coqide + $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,coqide + $ dune install --prefix= rocq-runtime coq-core rocq-core coq coqide-server coqide You can drop the `coqide` packages if not needed. diff --git a/Makefile b/Makefile index f4673633914f..71d914c88567 100644 --- a/Makefile +++ b/Makefile @@ -82,7 +82,7 @@ dev-targets: @echo "files that world will build. We provide some useful subtargets here:" @echo "" @echo " - theories-foo: for each directory theories/Foo, build the vo files for it and set them up in _build/install/default." - @echo " For instance the init target builds the prelude, combined with coq-core.install it produces a fully functional layout in _build/install/default." + @echo " For instance the init target builds the prelude, combined with rocq-runtime.install it produces a fully functional layout in _build/install/default." help-install: @echo "" @@ -91,16 +91,18 @@ help-install: @echo "" @echo " $$ ./configure -prefix " @echo " $$ make dunestrap" - @echo " $$ dune build -p coq-core,rocq-core" - @echo " $$ dune install --prefix= coq-core rocq-core" + @echo " $$ dune build -p rocq-runtime,coq-core,rocq-core" + @echo " $$ dune install --prefix= rocq-runtime coq-core rocq-core" @echo "" @echo " Provided opam/dune packages are:" @echo "" - @echo " - coq-core: base Coq package, toplevel compilers, plugins, tools, no stdlib, no GTK" + @echo " - rocq-runtime: base Rocq package, toplevel compilers, plugins, tools, no stdlib, no GTK" + @echo " - coq-core: compat binaries (coqc instead of rocq compile, etc)" @echo " - rocq-core: Coq's prelude and basis of standard library" @echo " - coqide-server: XML protocol language server" @echo " - coqide: CoqIDE gtk application" - @echo " - coq: meta package depending on coq-core rocq-core coq-stdlib" + @echo " - coq: meta package depending on rocq-runtime coq-core rocq-core coq-stdlib" + @echo " (also calls the test suite when using --with-test)" @echo "" @echo " To build a package, you can use:" @echo "" @@ -127,7 +129,7 @@ DUNESTRAPOPT=--root . # We regenerate always as to correctly track deps, can do better # We do a single call to dune as to avoid races and locking -ifneq ($(COQ_SPLIT),) # avoid depending on local coq-core +ifneq ($(COQ_SPLIT),) # avoid depending on local rocq-runtime _build/default/theories_dune_split _build/default/ltac2_dune_split .dune-stamp: FORCE dune build $(DUNEOPT) $(DUNESTRAPOPT) theories_dune_split ltac2_dune_split touch .dune-stamp @@ -158,7 +160,7 @@ dunestrap: $(DUNE_FILES) states: dunestrap dune build $(DUNEOPT) dev/shim/coqtop -MAIN_TARGETS:=coq-core.install rocq-core.install coqide-server.install +MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install coqide-server.install world: dunestrap dune build $(DUNEOPT) $(MAIN_TARGETS) @@ -232,8 +234,8 @@ CONTEXT=_build/install/default # XXX: Port this to a dune alias so the build is hygienic! .PHONY: plugin-tutorial plugin-tutorial: dunestrap - dune build $(CONTEXT)/lib/coq-core/META coq-core.install theories/Init/Prelude.vo - +$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN=$(shell pwd)/$(CONTEXT)/bin/ COQCORELIB=$(shell pwd)/$(CONTEXT)/lib/coq-core COQLIB=$(shell pwd)/_build/default/ -C doc/plugin_tutorial + dune build $(CONTEXT)/lib/rocq-runtime/META rocq-runtime.install theories/Init/Prelude.vo + +$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN=$(shell pwd)/$(CONTEXT)/bin/ COQCORELIB=$(shell pwd)/$(CONTEXT)/lib/rocq-runtime COQLIB=$(shell pwd)/_build/default/ -C doc/plugin_tutorial # This is broken in a very weird way with a permission error... see # the rule in doc/plugin_tutorial/dune: @@ -276,7 +278,7 @@ $(foreach subdir,$(wildcard theories/*/),$(eval $(call subtarget,$(subdir),$(she # Other common dev targets: # -# dune build coq-core.install +# dune build rocq-runtime.install # dune build coq.install # dune build coqide.install # diff --git a/boot/dune b/boot/dune index f5d33a647f3a..9ae2f69117c3 100644 --- a/boot/dune +++ b/boot/dune @@ -2,8 +2,12 @@ ; dependency for most Coq command line tools. (library (name boot) - (public_name coq-core.boot) + (public_name rocq-runtime.boot) (synopsis "Coq Enviroment and Paths facilities") ; until ocaml/dune#4892 fixed ; (private_modules util) - (libraries coq-core.config)) + (libraries rocq-runtime.config)) + +(deprecated_library_name + (old_public_name coq-core.boot) + (new_public_name rocq-runtime.boot)) diff --git a/boot/env.ml b/boot/env.ml index 61a249ce8362..af97ac078849 100644 --- a/boot/env.ml +++ b/boot/env.ml @@ -18,7 +18,7 @@ module Path = struct end -(* For now just a pointer to coq/lib (for .vo) and coq-core/lib (for plugins) *) +(* For now just a pointer to coq/lib (for .vo) and rocq-runtime/lib (for plugins) *) type t = { core: Path.t ; lib : Path.t @@ -52,7 +52,7 @@ let guess_coqlib () = let guess_coqcorelib lib = if Sys.file_exists (Path.relative lib plugins_dir) then lib - else Path.relative lib "../coq-core" + else Path.relative lib "../rocq-runtime" let fail_lib lib = let open Printf in @@ -66,7 +66,7 @@ let fail_core plugin = let open Printf in eprintf "File not found: %s\n" plugin; eprintf "The path for Coq plugins is wrong.\n"; - eprintf "Coq plugins are shipped in the coq-core package.\n"; + eprintf "Coq plugins are shipped in the rocq-runtime package.\n"; eprintf "Please check the COQCORELIB env variable.\n"; exit 1 diff --git a/boot/env.mli b/boot/env.mli index 7d928bc174ba..42d60759088c 100644 --- a/boot/env.mli +++ b/boot/env.mli @@ -35,7 +35,7 @@ but we may do so in the future. Rules for "coqlib" are: - if none of the above succeeds, the initialization will fail - The [COQCORELIB] env variable is also used if set, if not, the location - of the coq-core files will be assumed to be [COQLIB/../coq-core], except + of the rocq-runtime files will be assumed to be [COQLIB/../rocq-runtime], except if [COQLIB/plugins] exists [as in some developers layouts], in which case we will set [COQCORELIB:=COQLIB]. @@ -96,7 +96,7 @@ val native_cmi : t -> string -> Path.t (** The location of the revision file *) val revision : t -> Path.t -(** coq-core/lib directory, not sure if to keep this *) +(** rocq-runtime/lib directory, not sure if to keep this *) val corelib : t -> Path.t (** coq/lib directory, not sure if to keep this *) diff --git a/checker/dune b/checker/dune index 1d4cc3d90c7f..32bbcd240af1 100644 --- a/checker/dune +++ b/checker/dune @@ -4,18 +4,22 @@ ; duplicate module names in the whole build. (library (name coq_checklib) - (public_name coq-core.checklib) + (public_name rocq-runtime.checklib) (synopsis "Rocq's Standalone Proof Checker") (modules :standard \ coqchk votour) (wrapped true) - (libraries coq-core.boot coq-core.kernel)) + (libraries rocq-runtime.boot rocq-runtime.kernel)) + +(deprecated_library_name + (old_public_name coq-core.checklib) + (new_public_name rocq-runtime.checklib)) (executable (name coqchk) (public_name coqchk) (modes exe byte) ; Move to coq-checker? - (package coq-core) + (package rocq-runtime) (modules coqchk) (flags :standard -open Coq_checklib) (libraries coq_checklib)) @@ -23,7 +27,7 @@ (executable (name votour) (public_name votour) - (package coq-core) + (package rocq-runtime) (modules votour) (flags :standard -open Coq_checklib) (libraries coq_checklib)) diff --git a/clib/dune b/clib/dune index 76b6970b407f..8b293908eb4a 100644 --- a/clib/dune +++ b/clib/dune @@ -1,7 +1,7 @@ (library (name clib) (synopsis "Coq's Utility Library [general purpose]") - (public_name coq-core.clib) + (public_name rocq-runtime.clib) (wrapped false) (modules_without_implementation cSig) (modules :standard \ unicodetable_gen) @@ -11,6 +11,10 @@ (memprof-limits -> memprof_coq.memprof.ml)) str unix threads)) +(deprecated_library_name + (old_public_name coq-core.clib) + (new_public_name rocq-runtime.clib)) + (executable (name unicodetable_gen) (modules unicodetable_gen)) diff --git a/config/dune b/config/dune index 6f74936be838..5307e7281d7f 100644 --- a/config/dune +++ b/config/dune @@ -1,19 +1,27 @@ (library (name config) (synopsis "Coq Configuration Variables") - (public_name coq-core.config) + (public_name rocq-runtime.config) (modules coq_config) (wrapped false)) +(deprecated_library_name + (old_public_name coq-core.config) + (new_public_name rocq-runtime.config)) + (library (name byte_config) (synopsis "Coq Configuration Variables (for bytecode only)") - (public_name coq-core.config.byte) + (public_name rocq-runtime.config.byte) (modules coq_byte_config) (wrapped false) (libraries compiler-libs.toplevel) (modes byte)) +(deprecated_library_name + (old_public_name coq-core.config.byte) + (new_public_name rocq-runtime.config.byte)) + (executable (name list_plugins) (modules list_plugins)) (rule (targets plugin_list) (deps (source_tree %{project_root}/plugins)) diff --git a/coq-core.opam b/coq-core.opam index 8dea4a73a6dc..3e965620088e 100644 --- a/coq-core.opam +++ b/coq-core.opam @@ -1,25 +1,7 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" version: "dev" -synopsis: "The Coq Proof Assistant -- Core Binaries and Tools" -description: """ -Coq is a formal proof management system. It provides -a formal language to write mathematical definitions, executable -algorithms and theorems together with an environment for -semi-interactive development of machine-checked proofs. - -Typical applications include the certification of properties of -programming languages (e.g. the CompCert compiler certification -project, or the Bedrock verified low-level programming library), the -formalization of mathematics (e.g. the full formalization of the -Feit-Thompson theorem or homotopy type theory) and teaching. - -This package includes the Coq core binaries, plugins, and tools, but -not the vernacular standard library. - -Note that in this setup, Coq needs to be started with the -boot and --noinit options, as will otherwise fail to find the regular Coq -prelude, now living in the rocq-core package.""" +synopsis: "Compatibility binaries for Coq after the Rocq renaming" maintainer: ["The Coq development team "] authors: ["The Coq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" @@ -28,22 +10,11 @@ doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" depends: [ "dune" {>= "3.8"} - "ocaml" {>= "4.09.0"} - "ocamlfind" {>= "1.8.1"} - "zarith" {>= "1.11"} - "conf-linux-libc-dev" {os = "linux"} + "rocq-runtime" {= version} "odoc" {with-doc} ] -depopts: ["coq-native" "memprof-limits" "memtrace"] -dev-repo: "git+https://github.com/coq/coq.git" build: [ ["dune" "subst"] {dev} - [ "./configure" - "-prefix" prefix - "-mandir" man - "-libdir" "%{lib}%/coq" - "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} - ] [ "dune" "build" @@ -51,10 +22,9 @@ build: [ name "-j" jobs - "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] - ["dune" "install" "-p" name "--create-install-files" name] ] +dev-repo: "git+https://github.com/coq/coq.git" diff --git a/coqide-server.opam b/coqide-server.opam index 06550a6c269e..e5c22ee147ae 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -20,7 +20,7 @@ doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" depends: [ "dune" {>= "3.8"} - "coq-core" {= version} + "rocq-runtime" {= version} "odoc" {with-doc} ] build: [ diff --git a/coqpp/dune b/coqpp/dune index e4cdc33b3d8c..6fdd7f598fb7 100644 --- a/coqpp/dune +++ b/coqpp/dune @@ -10,6 +10,6 @@ (executable (name coqpp_main) (public_name coqpp) - (package coq-core) + (package rocq-runtime) (libraries coqpp) (modules coqpp_main)) diff --git a/default.nix b/default.nix index 8652a3a0faf9..c9bcec991941 100644 --- a/default.nix +++ b/default.nix @@ -120,7 +120,7 @@ stdenv.mkDerivation rec { # From https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/ocaml/dune.nix installPhase = '' runHook preInstall - dune install --prefix $out --libdir $OCAMLFIND_DESTDIR coq-core rocq-core coqide-server ${optionalString buildIde "coqide"} + dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core coqide-server ${optionalString buildIde "coqide"} runHook postInstall ''; @@ -131,7 +131,7 @@ stdenv.mkDerivation rec { createFindlibDestdir = !shell; - postInstall = "ln -s $out/lib/coq-core $OCAMLFIND_DESTDIR/coq-core"; + postInstall = "ln -s $out/lib/rocq-runtime $OCAMLFIND_DESTDIR/rocq-runtime && ln -s $out/lib/coq-core $OCAMLFIND_DESTDIR/coq-core"; inherit doInstallCheck; diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh index e8747bb21c02..8198170a65f5 100755 --- a/dev/bench/bench.sh +++ b/dev/bench/bench.sh @@ -462,7 +462,7 @@ export PROFILING=1 export COQ_PROFILE_COMPONENTS=command,parse_command,partac.perform # packages tied to the coq commit need to be pinned accordingly -core_packages='coq-core rocq-core coq-stdlib coqide-server coq' +core_packages='rocq-runtime coq-core rocq-core coq-stdlib coqide-server coq' for coq_opam_package in $core_packages $coq_opam_packages; do @@ -509,7 +509,8 @@ $coq_opam_package (unknown package)" git checkout -q $COQ_HASH - if [ "$coq_opam_package" = rocq-core ] && ! [ -e $coq_opam_package.opam ]; then + if { [ "$coq_opam_package" = rocq-core ] || [ "$coq_opam_package" = rocq-runtime ]; } \ + && ! [ -e $coq_opam_package.opam ]; then echo "Skipping $coq_opam_package for $RUNNER" continue 2 fi diff --git a/dev/bench/dune b/dev/bench/dune index a1ccb90b670f..198933f82946 100644 --- a/dev/bench/dune +++ b/dev/bench/dune @@ -21,6 +21,6 @@ (executable (name timelog2html) (public_name coqtimelog2html) - (package coq-core) + (package rocq-runtime) (modules timelog2html) (libraries benchlib)) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index c6ce4c4ea297..330908f9b841 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -33,7 +33,7 @@ then export OCAMLPATH="$PWD/_build/install/default/lib/$OCAMLFINDSEP$OCAMLPATH" export COQBIN="$PWD/_build/install/default/bin" export COQLIB="$PWD/_build/install/default/lib/coq" - export COQCORELIB="$PWD/_build/install/default/lib/coq-core" + export COQCORELIB="$PWD/_build/install/default/lib/rocq-runtime" CI_INSTALL_DIR="$PWD/_build/install/default/" diff --git a/dev/ci/platform/coq-pf-03-build.bat b/dev/ci/platform/coq-pf-03-build.bat index 878685fc83fe..434678e360a8 100644 --- a/dev/ci/platform/coq-pf-03-build.bat +++ b/dev/ci/platform/coq-pf-03-build.bat @@ -21,6 +21,7 @@ call coq_platform_make_windows.bat ^ -jobs=2 ^ -switch=d ^ -set-switch=y ^ + -override-dev-pkg="rocq-runtime=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^ -override-dev-pkg="coq-core=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^ -override-dev-pkg="rocq-core=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^ -override-dev-pkg="coq=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^ diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 4c27a39f57aa..e5cd61f6655e 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -68,7 +68,7 @@ tweak some low-level option. Dune is able to build all the OCaml parts of Coq in a pretty standard way, using its built-in rule generation for OCaml. Public tools -written in OCaml are distributed in the `coq-core` package. +written in OCaml are distributed in the `rocq-runtime` package. The set of public `.v` files present in this repository, usually referred as the "Coq prelude" are distributed in the @@ -140,8 +140,8 @@ for example, to add plugins to be linked statically using the Note that Coq relies on a hidden Dune hack, which will add `-linkall` to binaries if they depend on the `findlib.dynload` library. As of -today, `coq-core.vernac` uses `findlib.dynload`, so if your toplevel -hooks at the `coq-core.vernac` or above level, you should be OK, +today, `rocq-runtime.vernac` uses `findlib.dynload`, so if your toplevel +hooks at the `rocq-runtime.vernac` or above level, you should be OK, otherwise add `-linkall` to Dune's `(link_flags ...)` field for your binary. @@ -233,7 +233,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. depending on the error) - If there is a linking error (eg from "source db"), do a "dune - build coq-core.install" and try again. + build rocq-runtime.install" and try again. ## Dropping from coqtop: diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index ff38370bd191..aa1fa7954b05 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -25,7 +25,7 @@ - [ ] For major releases, you can create new views in the above project (on the model of previous releases) - [ ] Pin the versions of libraries and plugins in [`dev/ci/ci-basic-overlay.sh`](../ci/ci-basic-overlay.sh) to use commit hashes. You can use the [`dev/tools/pin-ci.sh`](../tools/pin-ci.sh) script to do this semi-automatically. - [ ] In a PR on `master` to be backported, add a new link to the `'versions'` list of the refman (in `html_context` in [`doc/sphinx/conf.py`](../../doc/sphinx/conf.py)). -- [ ] Add `{coq-core,rocq-core,coqide-server}.X.X.dev` packages in [`core-dev`](https://github.com/coq/opam-coq-archive/tree/master/core-dev) +- [ ] Add `{rocq-runtime,coq-core,rocq-core,coqide-server}.X.X.dev` packages in [`core-dev`](https://github.com/coq/opam-coq-archive/tree/master/core-dev) - [ ] Ensure a `coq-stdlib` package compatible with the new packages above exists either in [`ocaml repo`](https://github.com/ocaml/opam-repository) or in [`core-dev`](https://github.com/coq/opam-coq-archive/tree/master/core-dev) - [ ] Add `coq.X.X.dev` package in [`core-dev`](https://github.com/coq/opam-coq-archive/tree/master/core-dev) - [ ] Ping `@erikmd` and `@Zimmi48` to set up the infrastructure to have alpha Docker images built for the branch: the main steps amount to release `coq-bignums v9.Y.Y+coqX.X` in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), prepare a new [Docker-Coq](https://github.com/coq-community/docker-coq) image `coqorg/coq:X.X-alpha`, then browse to copy the `dev` webhook into a new `vX.X` webhook: `https://gitlab.com/api/v4/projects/19687072/trigger/pipeline?ref=master&variables[CRON_MODE]=rebuild-keyword&variables[ITEM]=X.X&token=_`, Push events → Wildcard pattern → `vX.X`, Test Push events. (If need be, the token can be regenerated at .) diff --git a/dev/dune b/dev/dune index e0985b5d63a7..0be52b8c51a7 100644 --- a/dev/dune +++ b/dev/dune @@ -1,21 +1,21 @@ (library (name dev) - (public_name coq-core.dev) + (public_name rocq-runtime.dev) (synopsis "Coq's Debug Printers") (wrapped false) (modules top_printers vm_printers) ; NB currently we have no "install_printer" using ltac2, ; but we still want to load_printer ltac2 ; so that its genarg printers are present in the debugger's printer process - (libraries coq-core.vernac coq-core.plugins.ltac coq-core.plugins.ltac2)) + (libraries rocq-runtime.vernac rocq-runtime.plugins.ltac rocq-runtime.plugins.ltac2)) (library (name debugger_support) - (public_name coq-core.debugger_support) + (public_name rocq-runtime.debugger_support) (synopsis "Coq Support for ocamldebug") (wrapped false) (modules debugger_support) - (libraries coq-core.dev)) + (libraries rocq-runtime.dev)) (rule (targets dune-dbg) @@ -29,28 +29,28 @@ ; We require all the OCaml libs to be in place and searchable ; by OCamlfind, this is a bit of a hack but until Dune gets ; proper ocamldebug support we have to live with that. - %{lib:coq-core.config:config.cma} - %{lib:coq-core.clib:clib.cma} - %{lib:coq-core.lib:lib.cma} - %{lib:coq-core.kernel:kernel.cma} - %{lib:coq-core.vm:coqrun.cma} - %{lib:coq-core.vm:../../stublibs/dllcoqrun_stubs.so} - %{lib:coq-core.library:library.cma} - %{lib:coq-core.engine:engine.cma} - %{lib:coq-core.pretyping:pretyping.cma} - %{lib:coq-core.gramlib:gramlib.cma} - %{lib:coq-core.interp:interp.cma} - %{lib:coq-core.proofs:proofs.cma} - %{lib:coq-core.parsing:parsing.cma} - %{lib:coq-core.printing:printing.cma} - %{lib:coq-core.tactics:tactics.cma} - %{lib:coq-core.vernac:vernac.cma} - %{lib:coq-core.plugins.ltac:ltac_plugin.cma} - %{lib:coq-core.plugins.ltac2:ltac2_plugin.cma} - %{lib:coq-core.dev:dev.cma} - %{lib:coq-core.debugger_support:debugger_support.cmi} - %{lib:coq-core.debugger_support:debugger_support.cma} - %{lib:coq-core.debugger_support:../META}) + %{lib:rocq-runtime.config:config.cma} + %{lib:rocq-runtime.clib:clib.cma} + %{lib:rocq-runtime.lib:lib.cma} + %{lib:rocq-runtime.kernel:kernel.cma} + %{lib:rocq-runtime.vm:coqrun.cma} + %{lib:rocq-runtime.vm:../../stublibs/dllcoqrun_stubs.so} + %{lib:rocq-runtime.library:library.cma} + %{lib:rocq-runtime.engine:engine.cma} + %{lib:rocq-runtime.pretyping:pretyping.cma} + %{lib:rocq-runtime.gramlib:gramlib.cma} + %{lib:rocq-runtime.interp:interp.cma} + %{lib:rocq-runtime.proofs:proofs.cma} + %{lib:rocq-runtime.parsing:parsing.cma} + %{lib:rocq-runtime.printing:printing.cma} + %{lib:rocq-runtime.tactics:tactics.cma} + %{lib:rocq-runtime.vernac:vernac.cma} + %{lib:rocq-runtime.plugins.ltac:ltac_plugin.cma} + %{lib:rocq-runtime.plugins.ltac2:ltac2_plugin.cma} + %{lib:rocq-runtime.dev:dev.cma} + %{lib:rocq-runtime.debugger_support:debugger_support.cmi} + %{lib:rocq-runtime.debugger_support:debugger_support.cma} + %{lib:rocq-runtime.debugger_support:../META}) (action (copy dune-dbg.in dune-dbg))) (alias @@ -59,7 +59,7 @@ (install (section lib) - (package coq-core) + (package rocq-runtime) (files (ml_toplevel/include as dev/ml_toplevel/include) (ml_toplevel/include_directories as dev/ml_toplevel/include_directories) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 6e3834124ef5..01c4d9b4ca8a 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -16,7 +16,7 @@ while [[ $# -gt 0 ]]; do coqchk) shift exe=_build/default/checker/coqchk.bc - opts+=($(ocamlfind query -recursive -i-format coq-core.checklib)) + opts+=($(ocamlfind query -recursive -i-format rocq-runtime.checklib)) break ;; coqide) @@ -51,4 +51,4 @@ while [[ $# -gt 0 ]]; do esac done -ocamldebug "${opts[@]}" $(ocamlfind query -recursive -i-format coq-core.dev) $(ocamlfind query -i-format -descendants coq-core.vernac) -I +threads -I dev $exe "$@" +ocamldebug "${opts[@]}" $(ocamlfind query -recursive -i-format rocq-runtime.dev) $(ocamlfind query -i-format -descendants rocq-runtime.vernac) -I +threads -I dev $exe "$@" diff --git a/dev/shim/dune b/dev/shim/dune index 551b6d2f71bf..a958ef38a8ac 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -66,30 +66,30 @@ (deps %{project_root}/theories/Init/Prelude.vo %{bin:coqtop.byte} - %{lib:coq-core.config:config.cma} - %{lib:coq-core.clib:clib.cma} - %{lib:coq-core.lib:lib.cma} - %{lib:coq-core.kernel:kernel.cma} - %{lib:coq-core.vm:coqrun.cma} - %{lib:coq-core.vm:../../stublibs/dllcoqrun_stubs.so} - %{lib:coq-core.library:library.cma} - %{lib:coq-core.engine:engine.cma} - %{lib:coq-core.pretyping:pretyping.cma} - %{lib:coq-core.gramlib:gramlib.cma} - %{lib:coq-core.interp:interp.cma} - %{lib:coq-core.proofs:proofs.cma} - %{lib:coq-core.parsing:parsing.cma} - %{lib:coq-core.printing:printing.cma} - %{lib:coq-core.tactics:tactics.cma} - %{lib:coq-core.vernac:vernac.cma} - %{lib:coq-core.stm:stm.cma} - %{lib:coq-core.sysinit:sysinit.cma} - %{lib:coq-core.toplevel:toplevel.cma} - %{lib:coq-core.plugins.number_string_notation:number_string_notation_plugin.cma} - %{lib:coq-core.plugins.tauto:tauto_plugin.cma} - %{lib:coq-core.plugins.cc:cc_plugin.cma} - %{lib:coq-core.plugins.firstorder:firstorder_plugin.cma} - %{lib:coq-core.plugins.ltac:ltac_plugin.cma} + %{lib:rocq-runtime.config:config.cma} + %{lib:rocq-runtime.clib:clib.cma} + %{lib:rocq-runtime.lib:lib.cma} + %{lib:rocq-runtime.kernel:kernel.cma} + %{lib:rocq-runtime.vm:coqrun.cma} + %{lib:rocq-runtime.vm:../../stublibs/dllcoqrun_stubs.so} + %{lib:rocq-runtime.library:library.cma} + %{lib:rocq-runtime.engine:engine.cma} + %{lib:rocq-runtime.pretyping:pretyping.cma} + %{lib:rocq-runtime.gramlib:gramlib.cma} + %{lib:rocq-runtime.interp:interp.cma} + %{lib:rocq-runtime.proofs:proofs.cma} + %{lib:rocq-runtime.parsing:parsing.cma} + %{lib:rocq-runtime.printing:printing.cma} + %{lib:rocq-runtime.tactics:tactics.cma} + %{lib:rocq-runtime.vernac:vernac.cma} + %{lib:rocq-runtime.stm:stm.cma} + %{lib:rocq-runtime.sysinit:sysinit.cma} + %{lib:rocq-runtime.toplevel:toplevel.cma} + %{lib:rocq-runtime.plugins.number_string_notation:number_string_notation_plugin.cma} + %{lib:rocq-runtime.plugins.tauto:tauto_plugin.cma} + %{lib:rocq-runtime.plugins.cc:cc_plugin.cma} + %{lib:rocq-runtime.plugins.firstorder:firstorder_plugin.cma} + %{lib:rocq-runtime.plugins.ltac:ltac_plugin.cma} (alias %{project_root}/dev/ml_toplevel_files))) (rule diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 5a2957c0cc3b..367aca507ecc 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -51,7 +51,7 @@ "Setup `compile-command' for Coq development." (let ((dir (coqdev-default-directory))) (when dir (setq-local compile-command (concat "cd " (shell-quote-argument dir) " -dune build @check # coq-core.install dev/shim/coqtop"))))) +dune build @check # rocq-runtime.install dev/shim/rocq"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) (defvar camldebug-command-name) ; from camldebug.el (caml package) diff --git a/doc/corelib/Library.tex b/doc/corelib/Library.tex index 7b1bb4346571..f66dd816d0e7 100644 --- a/doc/corelib/Library.tex +++ b/doc/corelib/Library.tex @@ -7,7 +7,7 @@ \usepackage{amsfonts} \usepackage{amssymb} \usepackage{url} -\usepackage[color]{../../lib/coq-core/tools/coqdoc/coqdoc} +\usepackage[color]{../../lib/rocq-runtime/tools/coqdoc/coqdoc} \input{../common/version} \input{../common/title} diff --git a/doc/corelib/dune b/doc/corelib/dune index fa603163fd60..5108fc76e467 100644 --- a/doc/corelib/dune +++ b/doc/corelib/dune @@ -22,6 +22,7 @@ (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. + (package rocq-runtime) (package coq-core) (package rocq-core)) (action diff --git a/doc/dune b/doc/dune index 579f9399904e..cbc94eaf5696 100644 --- a/doc/dune +++ b/doc/dune @@ -13,6 +13,7 @@ ; + %{bin:coqdoc} etc... ; + config/coq_config.py ; + tools/coqdoc/coqdoc.css + (package rocq-runtime) (package coq-core) (package rocq-core) (source_tree sphinx) @@ -30,6 +31,7 @@ ; (deps (alias refman-deps)) ; EJGA: note this should've been fixed in dune master as of 05/03/2021 (deps + (package rocq-runtime) (package coq-core) (package rocq-core) (source_tree sphinx) @@ -50,6 +52,7 @@ ; (deps (alias refman-deps)) ; EJGA: note this should've been fixed in dune master as of 05/03/2021 (deps + (package rocq-runtime) (package coq-core) (package rocq-core) (source_tree sphinx) diff --git a/doc/plugin_tutorial/dune b/doc/plugin_tutorial/dune index 92f60ba9d240..0571cf8fa6fe 100644 --- a/doc/plugin_tutorial/dune +++ b/doc/plugin_tutorial/dune @@ -3,7 +3,7 @@ ; (alias plugin-tutorial) ; (deps ; (source_tree .) -; (package coq-core) +; (package rocq-runtime) ; ../../tools/CoqMakefile.in ; ../../theories/Init/Prelude.vo) ; (action diff --git a/doc/plugin_tutorial/tuto0/src/META.coq-plugin-tutorial b/doc/plugin_tutorial/tuto0/src/META.coq-plugin-tutorial index 8320663faac2..2aafedcc0e6d 100644 --- a/doc/plugin_tutorial/tuto0/src/META.coq-plugin-tutorial +++ b/doc/plugin_tutorial/tuto0/src/META.coq-plugin-tutorial @@ -2,7 +2,7 @@ package "tuto0" ( directory = "." version = "dev" description = "A tuto0 plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "tuto0_plugin.cma" archive(native) = "tuto0_plugin.cmxa" plugin(byte) = "tuto0_plugin.cma" diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune index c7ed997221e9..32a15ea4710a 100644 --- a/doc/plugin_tutorial/tuto0/src/dune +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -1,6 +1,6 @@ (library (name tuto0_plugin) - (public_name coq-core.plugins.tutorial.p0) - (libraries coq-core.plugins.ltac)) + (public_name rocq-runtime.plugins.tutorial.p0) + (libraries rocq-runtime.plugins.ltac)) (coq.pp (modules g_tuto0)) diff --git a/doc/plugin_tutorial/tuto1/src/META.coq-plugin-tutorial b/doc/plugin_tutorial/tuto1/src/META.coq-plugin-tutorial index 17ec4d6dec99..f35e03d21f22 100644 --- a/doc/plugin_tutorial/tuto1/src/META.coq-plugin-tutorial +++ b/doc/plugin_tutorial/tuto1/src/META.coq-plugin-tutorial @@ -2,7 +2,7 @@ package "tuto1" ( directory = "." version = "dev" description = "A tuto1 plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "tuto1_plugin.cma" archive(native) = "tuto1_plugin.cmxa" plugin(byte) = "tuto1_plugin.cma" diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune index bf87222e16dc..0754ae6b1034 100644 --- a/doc/plugin_tutorial/tuto1/src/dune +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -1,6 +1,6 @@ (library (name tuto1_plugin) - (public_name coq-core.plugins.tutorial.p1) - (libraries coq-core.plugins.ltac)) + (public_name rocq-runtime.plugins.tutorial.p1) + (libraries rocq-runtime.plugins.ltac)) (coq.pp (modules g_tuto1)) diff --git a/doc/plugin_tutorial/tuto2/src/META.coq-plugin-tutorial b/doc/plugin_tutorial/tuto2/src/META.coq-plugin-tutorial index ca56ba411789..64306f1c84e6 100644 --- a/doc/plugin_tutorial/tuto2/src/META.coq-plugin-tutorial +++ b/doc/plugin_tutorial/tuto2/src/META.coq-plugin-tutorial @@ -2,7 +2,7 @@ package "tuto2" ( directory = "." version = "dev" description = "A tuto2 plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "tuto2_plugin.cma" archive(native) = "tuto2_plugin.cmxa" plugin(byte) = "tuto2_plugin.cma" diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index 0797debccf7d..11153897f500 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -1,6 +1,6 @@ (library (name tuto2_plugin) - (public_name coq-core.plugins.tutorial.p2) - (libraries coq-core.plugins.ltac)) + (public_name rocq-runtime.plugins.tutorial.p2) + (libraries rocq-runtime.plugins.ltac)) (coq.pp (modules g_tuto2)) diff --git a/doc/plugin_tutorial/tuto3/src/META.coq-plugin-tutorial b/doc/plugin_tutorial/tuto3/src/META.coq-plugin-tutorial index a6887a154318..237683f84c4b 100644 --- a/doc/plugin_tutorial/tuto3/src/META.coq-plugin-tutorial +++ b/doc/plugin_tutorial/tuto3/src/META.coq-plugin-tutorial @@ -2,7 +2,7 @@ package "tuto3" ( directory = "." version = "dev" description = "A tuto3 plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "tuto3_plugin.cma" archive(native) = "tuto3_plugin.cmxa" plugin(byte) = "tuto3_plugin.cma" diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune index dcecf0852eeb..c1cb39e518e6 100644 --- a/doc/plugin_tutorial/tuto3/src/dune +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -1,7 +1,7 @@ (library (name tuto3_plugin) - (public_name coq-core.plugins.tutorial.p3) + (public_name rocq-runtime.plugins.tutorial.p3) (flags :standard -warn-error -3) - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) (coq.pp (modules g_tuto3)) diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index ccd9b0f87d98..7f4667b6b079 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -1220,7 +1220,7 @@ The preferred method is to use ``dune``: (executable (name my_toplevel) - (libraries coq-core.toplevel)) + (libraries rocq-runtime.toplevel)) in a directory with `my_toplevel.ml` containing the main loop entry point `Coqc.main()` or `Coqtop.(start_coq coqtop_toplevel)` (depending @@ -1232,7 +1232,7 @@ For example, to statically link |Ltac|, you can do: (executable (name my_toplevel) - (libraries coq-core.toplevel coq-core.plugins.ltac)) + (libraries rocq-runtime.toplevel rocq-runtime.plugins.ltac)) and similarly for other plugins. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 6de1b98ad45f..35f8f8202eb9 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -668,7 +668,7 @@ file is a particular case of a module called a *library file*. Loads OCaml plugins and their dependencies dynamically. The :n:`@string` arguments must be valid `findlib `_ - plugin names, for example ``coq-core.plugins.ltac``. + plugin names, for example ``rocq-runtime.plugins.ltac``. Effects (such as adding new commands) from the explicitly requested plugin are activated, but effects from implicitly loaded @@ -713,8 +713,8 @@ file is a particular case of a module called a *library file*. The plugin declaration in some ``.mlg`` file does not match the ``findlib`` plugin name. In the example of - ``coq-core.plugins.ltac``, one has to write ``DECLARE PLUGIN - "coq-core.plugins.ltac"``. + ``rocq-runtime.plugins.ltac``, one has to write ``DECLARE PLUGIN + "rocq-runtime.plugins.ltac"``. .. cmd:: Print ML Modules diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 89937893cbe8..071acef69229 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -1,6 +1,6 @@ (executable (name doc_grammar) - (libraries coq-core.clib coqpp)) + (libraries rocq-runtime.clib coqpp)) (env (_ (binaries doc_grammar.exe))) diff --git a/dune b/dune index e01e0236331b..8260a9309d3c 100644 --- a/dune +++ b/dune @@ -21,11 +21,11 @@ (alias (name default) - (deps coq-core.install rocq-core.install coqide-server.install)) + (deps rocq-runtime.install coq-core.install rocq-core.install coqide-server.install)) (install (section lib) - (package coq-core) + (package rocq-runtime) (files revision)) (rule @@ -41,7 +41,7 @@ (source_tree plugins) (source_tree theories) (source_tree user-contrib) - %{workspace_root}/_build/install/%{context_name}/lib/coq-core/META) + %{workspace_root}/_build/install/%{context_name}/lib/rocq-runtime/META) (action (with-stdout-to %{targets} (run tools/dune_rule_gen/gen_rules.exe Corelib theories %{env:COQ_DUNE_EXTRA_OPT=})))) @@ -52,7 +52,7 @@ (source_tree plugins) (source_tree theories) (source_tree user-contrib) - %{workspace_root}/_build/install/%{context_name}/lib/coq-core/META) + %{workspace_root}/_build/install/%{context_name}/lib/rocq-runtime/META) (action (with-stdout-to %{targets} (run tools/dune_rule_gen/gen_rules.exe Ltac2 user-contrib/Ltac2 %{env:COQ_DUNE_EXTRA_OPT=})))) diff --git a/dune-project b/dune-project index 136ec1a4a99f..21109897ec75 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,5 @@ (lang dune 3.8) -(name coq) +(name rocq) ; We use directory targets in documentation (using directory-targets 0.1) @@ -24,7 +24,7 @@ ; Note that we use coq.opam.template to have dune add the correct opam ; prefix for configure (package - (name coq-core) + (name rocq-runtime) (depends (ocaml (>= 4.09.0)) (ocamlfind (>= 1.8.1)) @@ -50,10 +50,16 @@ Note that in this setup, Coq needs to be started with the -boot and -noinit options, as will otherwise fail to find the regular Coq prelude, now living in the rocq-core package.")) +(package + (name coq-core) + (depends + (rocq-runtime (= :version))) + (synopsis "Compatibility binaries for Coq after the Rocq renaming")) + (package (name rocq-core) (depends - (coq-core (= :version))) + (rocq-runtime (= :version))) (depopts coq-native) (synopsis "The Coq Proof Assistant with its prelude") (description "Coq is a formal proof management system. It provides @@ -74,7 +80,7 @@ Corelib.* and Ltac2.* namespaces.")) (package (name coqide-server) (depends - (coq-core (= :version))) + (rocq-runtime (= :version))) (synopsis "The Coq Proof Assistant, XML protocol server") (description "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable diff --git a/engine/dune b/engine/dune index f95496ded229..9bf6d0b8346f 100644 --- a/engine/dune +++ b/engine/dune @@ -1,8 +1,12 @@ (library (name engine) (synopsis "Coq's Tactic Engine") - (public_name coq-core.engine) + (public_name rocq-runtime.engine) (wrapped false) ; until ocaml/dune#4892 fixed ; (private_modules univSubst) (libraries library)) + +(deprecated_library_name + (old_public_name coq-core.engine) + (new_public_name rocq-runtime.engine)) diff --git a/gramlib/dune b/gramlib/dune index d6be1357ba1f..de64e44fed3d 100644 --- a/gramlib/dune +++ b/gramlib/dune @@ -1,5 +1,9 @@ (library (name gramlib) - (public_name coq-core.gramlib) + (public_name rocq-runtime.gramlib) (modules_without_implementation plexing) - (libraries coq-core.lib)) + (libraries rocq-runtime.lib)) + +(deprecated_library_name + (old_public_name coq-core.gramlib) + (new_public_name rocq-runtime.gramlib)) diff --git a/ide/coqide/dune b/ide/coqide/dune index 0760a128d827..d0d6de07fe06 100644 --- a/ide/coqide/dune +++ b/ide/coqide/dune @@ -6,14 +6,14 @@ (public_name coqide-server.core) (wrapped false) (modules document) - (libraries coq-core.boot coq-core.lib)) + (libraries rocq-runtime.boot rocq-runtime.lib)) (executable (name idetop) (public_name coqidetop) (package coqide-server) (modules idetop) - (libraries coq-core.toplevel coqide-server.protocol platform_specific) + (libraries rocq-runtime.toplevel coqide-server.protocol platform_specific) (link_flags -linkall)) ; IDE Client, we may want to add the macos_prehook.ml conditionally. diff --git a/ide/coqide/protocol/dune b/ide/coqide/protocol/dune index 9e8eb47dd5d8..955f12f545c9 100644 --- a/ide/coqide/protocol/dune +++ b/ide/coqide/protocol/dune @@ -3,6 +3,6 @@ (public_name coqide-server.protocol) (wrapped false) (modules_without_implementation interface) - (libraries coq-core.lib)) + (libraries rocq-runtime.lib)) (ocamllex xml_lexer) diff --git a/index.mld b/index.mld index 80155f0f61c3..f0a1d31eb3d1 100644 --- a/index.mld +++ b/index.mld @@ -1,5 +1,5 @@ {0 coq } -The coq package is a virtual package gathering the rocq-core and coq-stdlib packages. +The coq package is a virtual package gathering the main Coq packages. -For the documentation of the OCaml API of Coq, see the {{: ../coq-core/index.html } coq-core } package. +For the documentation of the OCaml API of Coq, see the {{: ../rocq-runtime/index.html } coq-core } package. diff --git a/interp/dune b/interp/dune index 3e004bf285ed..830f64ce2068 100644 --- a/interp/dune +++ b/interp/dune @@ -1,7 +1,11 @@ (library (name interp) (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]") - (public_name coq-core.interp) + (public_name rocq-runtime.interp) (wrapped false) (modules_without_implementation constrexpr notation_term) (libraries zarith pretyping gramlib)) + +(deprecated_library_name + (old_public_name coq-core.interp) + (new_public_name rocq-runtime.interp)) diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 4d1d28e4896f..a152f1fe5a05 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -1,12 +1,16 @@ (library (name coqrun) (synopsis "Rocq's Kernel Abstract Reduction Machine [C implementation]") - (public_name coq-core.vm) + (public_name rocq-runtime.vm) (foreign_stubs (language c) (names rocq_fix_code rocq_float64 rocq_memory rocq_values rocq_interp) (flags :standard (:include %{project_root}/config/dune.c_flags)))) +(deprecated_library_name + (old_public_name coq-core.vm) + (new_public_name rocq-runtime.vm)) + (rule (targets rocq_instruct.h) (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum)))) diff --git a/kernel/dune b/kernel/dune index d9277455e0bb..abb32f10fa04 100644 --- a/kernel/dune +++ b/kernel/dune @@ -1,12 +1,16 @@ (library (name kernel) (synopsis "The Coq Kernel") - (public_name coq-core.kernel) + (public_name rocq-runtime.kernel) (wrapped false) (modules_without_implementation values declarations entries) (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries boot lib coqrun dynlink)) +(deprecated_library_name + (old_public_name coq-core.kernel) + (new_public_name rocq-runtime.kernel)) + (executable (name genOpcodeFiles) (modules genOpcodeFiles)) @@ -30,7 +34,7 @@ (action (copy# %{gen-file} %{targets}))) (documentation - (package coq-core)) + (package rocq-runtime)) ; In dev profile, we check the kernel against a more strict set of ; warnings. @@ -39,4 +43,4 @@ (deprecated_library_name (old_public_name coq.kernel) - (new_public_name coq-core.kernel)) + (new_public_name rocq-runtime.kernel)) diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index f9890c10bb93..4705d7eb8654 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -103,7 +103,7 @@ val override_unknown_warning : bool ref "-w -unknown-warning". *) module CoreCategories : sig - (** Categories used in coq-core. Might not be exhaustive. *) + (** Categories used in rocq-runtime. Might not be exhaustive. *) val automation : category val bytecode_compiler : category diff --git a/lib/dune b/lib/dune index e7b1418c9b42..d55aa49ac9c2 100644 --- a/lib/dune +++ b/lib/dune @@ -1,11 +1,15 @@ (library (name lib) (synopsis "Coq's Utility Library [coq-specific]") - (public_name coq-core.lib) + (public_name rocq-runtime.lib) (wrapped false) (modules_without_implementation xml_datatype) (libraries - coq-core.boot coq-core.clib coq-core.config + rocq-runtime.boot rocq-runtime.clib rocq-runtime.config (select instr.ml from (!coqperf -> instr.noperf.ml) (coqperf -> instr.perf.ml)))) + +(deprecated_library_name + (old_public_name coq-core.lib) + (new_public_name rocq-runtime.lib)) diff --git a/library/dune b/library/dune index bf90511ead9d..51d0b2b22db0 100644 --- a/library/dune +++ b/library/dune @@ -1,9 +1,10 @@ (library (name library) (synopsis "Coq's Loadable Libraries (vo) Support") - (public_name coq-core.library) + (public_name rocq-runtime.library) (wrapped false) (libraries kernel)) -(documentation - (package coq-core)) +(deprecated_library_name + (old_public_name coq-core.library) + (new_public_name rocq-runtime.library)) diff --git a/parsing/dune b/parsing/dune index a51526f66c6d..8f3ae8639a70 100644 --- a/parsing/dune +++ b/parsing/dune @@ -1,8 +1,12 @@ (library (name parsing) - (public_name coq-core.parsing) + (public_name rocq-runtime.parsing) (wrapped false) (modules_without_implementation notation_gram) - (libraries coq-core.gramlib interp)) + (libraries rocq-runtime.gramlib interp)) + +(deprecated_library_name + (old_public_name coq-core.parsing) + (new_public_name rocq-runtime.parsing)) (coq.pp (modules g_prim g_constr)) diff --git a/perf/dune b/perf/dune index 4fe5923874bd..561ee7eda48e 100644 --- a/perf/dune +++ b/perf/dune @@ -1,7 +1,7 @@ (library (name coqperf) (synopsis "Instruction count using Linux perf.") - (public_name coq-core.perf) + (public_name rocq-runtime.perf) (wrapped false) (foreign_stubs (language c) (names perf)) ; Just "linux" is not enough, see https://github.com/ocaml/dune/issues/4895. @@ -12,3 +12,7 @@ (= %{system} "linux_eabihf") (= %{system} "linux_elf") (= %{system} "elf")))) + +(deprecated_library_name + (old_public_name coq-core.perf) + (new_public_name rocq-runtime.perf)) diff --git a/plugins/btauto/dune b/plugins/btauto/dune index d1dbcc7a9d04..4ed87eb8dae8 100644 --- a/plugins/btauto/dune +++ b/plugins/btauto/dune @@ -1,7 +1,11 @@ (library (name btauto_plugin) - (public_name coq-core.plugins.btauto) + (public_name rocq-runtime.plugins.btauto) (synopsis "Rocq's btauto plugin") - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.btauto) + (new_public_name rocq-runtime.plugins.btauto)) (coq.pp (modules g_btauto)) diff --git a/plugins/btauto/g_btauto.mlg b/plugins/btauto/g_btauto.mlg index 0a8fb87c18a5..bc2760bf291d 100644 --- a/plugins/btauto/g_btauto.mlg +++ b/plugins/btauto/g_btauto.mlg @@ -14,7 +14,7 @@ open Ltac_plugin } -DECLARE PLUGIN "coq-core.plugins.btauto" +DECLARE PLUGIN "rocq-runtime.plugins.btauto" TACTIC EXTEND btauto | [ "btauto" ] -> { Refl_btauto.Btauto.tac } diff --git a/plugins/cc/dune b/plugins/cc/dune index 478d59c27114..e4ae27c4a83e 100644 --- a/plugins/cc/dune +++ b/plugins/cc/dune @@ -1,16 +1,24 @@ (library (name cc_core_plugin) - (public_name coq-core.plugins.cc_core) + (public_name rocq-runtime.plugins.cc_core) (synopsis "Rocq's congruence closure plugin") (modules (:standard \ g_congruence)) - (libraries coq-core.tactics)) + (libraries rocq-runtime.tactics)) + +(deprecated_library_name + (old_public_name coq-core.plugins.cc_core) + (new_public_name rocq-runtime.plugins.cc_core)) (library (name cc_plugin) - (public_name coq-core.plugins.cc) + (public_name rocq-runtime.plugins.cc) (synopsis "Rocq's congruence closure plugin (Ltac1 syntax)") (modules g_congruence) (flags :standard -open Cc_core_plugin) - (libraries coq-core.plugins.ltac coq-core.plugins.cc_core)) + (libraries rocq-runtime.plugins.ltac rocq-runtime.plugins.cc_core)) + +(deprecated_library_name + (old_public_name coq-core.plugins.cc) + (new_public_name rocq-runtime.plugins.cc)) (coq.pp (modules g_congruence)) diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg index 0005baf2ab3e..18523d39938b 100644 --- a/plugins/cc/g_congruence.mlg +++ b/plugins/cc/g_congruence.mlg @@ -16,7 +16,7 @@ open Stdarg } -DECLARE PLUGIN "coq-core.plugins.cc" +DECLARE PLUGIN "rocq-runtime.plugins.cc" (* Tactic registration *) diff --git a/plugins/derive/dune b/plugins/derive/dune index 28986a9f4fa0..ce2fac8d320c 100644 --- a/plugins/derive/dune +++ b/plugins/derive/dune @@ -1,7 +1,11 @@ (library (name derive_plugin) - (public_name coq-core.plugins.derive) + (public_name rocq-runtime.plugins.derive) (synopsis "Rocq's derive plugin") - (libraries coq-core.vernac)) + (libraries rocq-runtime.vernac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.derive) + (new_public_name rocq-runtime.plugins.derive)) (coq.pp (modules g_derive)) diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 6b9710c6b68a..efcad74a10af 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -14,14 +14,14 @@ open Stdarg } -DECLARE PLUGIN "coq-core.plugins.derive" +DECLARE PLUGIN "rocq-runtime.plugins.derive" { let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) let () = - Mltop.add_init_function "coq-core.plugins.derive" (fun () -> + Mltop.add_init_function "rocq-runtime.plugins.derive" (fun () -> Procq.(set_keyword_state (CLexer.add_keyword_tok (get_keyword_state ()) (Tok.PKEYWORD "SuchThat")))) let warn_deprecated_derive_suchthat = diff --git a/plugins/extraction/dune b/plugins/extraction/dune index 9bb8e87d5406..03650e691e4a 100644 --- a/plugins/extraction/dune +++ b/plugins/extraction/dune @@ -1,7 +1,11 @@ (library (name extraction_plugin) - (public_name coq-core.plugins.extraction) + (public_name rocq-runtime.plugins.extraction) (synopsis "Rocq's extraction plugin") - (libraries coq-core.vernac)) + (libraries rocq-runtime.vernac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.extraction) + (new_public_name rocq-runtime.plugins.extraction)) (coq.pp (modules g_extraction)) diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 6ebfc8da2bd1..4151e8f28c7c 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -14,7 +14,7 @@ open Procq.Prim } -DECLARE PLUGIN "coq-core.plugins.extraction" +DECLARE PLUGIN "rocq-runtime.plugins.extraction" { diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune index 47d31fc7ac92..087e5234b27f 100644 --- a/plugins/firstorder/dune +++ b/plugins/firstorder/dune @@ -1,16 +1,24 @@ (library (name firstorder_core_plugin) - (public_name coq-core.plugins.firstorder_core) + (public_name rocq-runtime.plugins.firstorder_core) (synopsis "Rocq's first order logic solver plugin") (modules (:standard \ g_ground)) - (libraries coq-core.tactics)) + (libraries rocq-runtime.tactics)) + +(deprecated_library_name + (old_public_name coq-core.plugins.firstorder_core) + (new_public_name rocq-runtime.plugins.firstorder_core)) (library (name firstorder_plugin) - (public_name coq-core.plugins.firstorder) + (public_name rocq-runtime.plugins.firstorder) (synopsis "Rocq's first order logic solver plugin (Ltac1 syntax)") (flags :standard -open Firstorder_core_plugin) (modules g_ground) - (libraries coq-core.plugins.firstorder_core coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.firstorder_core rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.firstorder) + (new_public_name rocq-runtime.plugins.firstorder)) (coq.pp (modules g_ground)) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 5b174e499ea8..3c7420c7e957 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -23,7 +23,7 @@ open Procq.Prim } -DECLARE PLUGIN "coq-core.plugins.firstorder" +DECLARE PLUGIN "rocq-runtime.plugins.firstorder" (* declaring search depth as a global option *) @@ -37,7 +37,7 @@ let { Goptions.get = ground_depth } = let default_intuition_tac = let tac _ _ = Auto.gen_auto None [] (Some []) in - let name = { Tacexpr.mltac_plugin = "coq-core.plugins.firstorder"; mltac_tactic = "auto_with"; } in + let name = { Tacexpr.mltac_plugin = "rocq-runtime.plugins.firstorder"; mltac_tactic = "auto_with"; } in let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in Tacenv.register_ml_tactic name [| tac |]; CAst.make (Tacexpr.TacML (entry, [])) diff --git a/plugins/funind/dune b/plugins/funind/dune index 81f7e04596da..e3eb56362370 100644 --- a/plugins/funind/dune +++ b/plugins/funind/dune @@ -1,7 +1,11 @@ (library (name funind_plugin) - (public_name coq-core.plugins.funind) + (public_name rocq-runtime.plugins.funind) (synopsis "Rocq's functional induction plugin") - (libraries coq-core.plugins.ltac coq-core.plugins.extraction)) + (libraries rocq-runtime.plugins.ltac rocq-runtime.plugins.extraction)) + +(deprecated_library_name + (old_public_name coq-core.plugins.funind) + (new_public_name rocq-runtime.plugins.funind)) (coq.pp (modules g_indfun)) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index d7eb50b3128d..b720ce0344db 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -26,7 +26,7 @@ open Pltac } -DECLARE PLUGIN "coq-core.plugins.funind" +DECLARE PLUGIN "rocq-runtime.plugins.funind" { diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index dc35b186adf2..6a451a624cbd 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -22,7 +22,7 @@ open Logic } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" (** Basic tactics *) @@ -322,11 +322,11 @@ let initial_atomic () = "fresh", CAst.make @@ TacArg(TacFreshId []) ] -let () = Mltop.declare_cache_obj initial_atomic "coq-core.plugins.ltac" +let () = Mltop.declare_cache_obj initial_atomic "rocq-runtime.plugins.ltac" (* First-class Ltac access to primitive blocks *) -let initial_name s = { mltac_plugin = "coq-core.plugins.ltac"; mltac_tactic = s; } +let initial_name s = { mltac_plugin = "rocq-runtime.plugins.ltac"; mltac_tactic = s; } let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; } let register_list_tactical name f = @@ -356,6 +356,6 @@ let initial_tacticals () = ([Name (idn 0)], CAst.make (TacML (initial_entry "solve", [varn 0])))); ] -let () = Mltop.declare_cache_obj initial_tacticals "coq-core.plugins.ltac" +let () = Mltop.declare_cache_obj initial_tacticals "rocq-runtime.plugins.ltac" } diff --git a/plugins/ltac/dune b/plugins/ltac/dune index aebe97a07654..d7ab8215bdfb 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -1,16 +1,24 @@ (library (name ltac_plugin) - (public_name coq-core.plugins.ltac) + (public_name rocq-runtime.plugins.ltac) (synopsis "Rocq's LTAC tactic language") (modules :standard \ tauto) (modules_without_implementation tacexpr) - (libraries coq-core.vernac)) + (libraries rocq-runtime.vernac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.ltac) + (new_public_name rocq-runtime.plugins.ltac)) (library (name tauto_plugin) - (public_name coq-core.plugins.tauto) + (public_name rocq-runtime.plugins.tauto) (synopsis "Rocq's tauto tactic") (modules tauto) - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.tauto) + (new_public_name rocq-runtime.plugins.tauto)) (coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 813f82209c63..01b22b8b24cf 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" { @@ -29,7 +29,7 @@ let () = G_ltac.for_extraargs let create_generic_quotation name e wit = let inject (loc, v) = Tacexpr.TacGeneric (Some name, Genarg.in_gen (Genarg.rawwit wit) v) in - Tacentries.create_ltac_quotation ~plugin:"coq-core.plugins.ltac" name inject (e, None) + Tacentries.create_ltac_quotation ~plugin:"rocq-runtime.plugins.ltac" name inject (e, None) let () = create_generic_quotation "integer" Procq.Prim.integer Stdarg.wit_int let () = create_generic_quotation "string" Procq.Prim.string Stdarg.wit_string @@ -44,7 +44,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl let () = create_generic_quotation "open_constr" Procq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation ~plugin:"coq-core.plugins.ltac" "ltac" inject (Pltac.ltac_expr, Some 5) + Tacentries.create_ltac_quotation ~plugin:"rocq-runtime.plugins.ltac" "ltac" inject (Pltac.ltac_expr, Some 5) (** Backward-compatible tactic notation entry names *) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 00681a922a8d..47fc4cbe0994 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -28,7 +28,7 @@ open G_redexpr } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" TACTIC EXTEND assert_succeeds | [ "assert_succeeds" tactic3(tac) ] diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 704a44a9efe5..573851ec2a80 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -19,7 +19,7 @@ open Hints } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" (* Hint bases *) diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 885491903ce2..c81232e84be2 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -16,7 +16,7 @@ open Classes } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" (** Options: depth, debug and transparency settings. *) diff --git a/plugins/ltac/g_eqdecide.mlg b/plugins/ltac/g_eqdecide.mlg index d967197058ea..3ceb8b253b60 100644 --- a/plugins/ltac/g_eqdecide.mlg +++ b/plugins/ltac/g_eqdecide.mlg @@ -21,7 +21,7 @@ open Stdarg } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" TACTIC EXTEND decide_equality | [ "decide" "equality" ] -> { decideEqualityGoal } diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 9c2c859c4d55..362c38b6d889 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" { diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index f6248ad9cf40..01c484ebc610 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -12,7 +12,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" { diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 77362ae00daf..d9f2edc283ba 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -31,7 +31,7 @@ open Vernacextend } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" { diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 519679feda60..63cd8997e2d5 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" { diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index 46dd3f0edd78..eac4acf685a3 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -17,7 +17,7 @@ open Stdarg } -DECLARE PLUGIN "coq-core.plugins.ltac" +DECLARE PLUGIN "rocq-runtime.plugins.ltac" { diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index bd2f83597872..d72b22984796 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -22,7 +22,7 @@ open Proofview.Notations module NamedDecl = Context.Named.Declaration -let tauto_plugin = "coq-core.plugins.tauto" +let tauto_plugin = "rocq-runtime.plugins.tauto" let () = Mltop.add_known_module tauto_plugin let assoc_var s ist = diff --git a/plugins/ltac2/dune b/plugins/ltac2/dune index 6019a8659b78..1163e7fbe7bb 100644 --- a/plugins/ltac2/dune +++ b/plugins/ltac2/dune @@ -1,8 +1,12 @@ (library (name ltac2_plugin) - (public_name coq-core.plugins.ltac2) + (public_name rocq-runtime.plugins.ltac2) (synopsis "Ltac2 plugin") (modules_without_implementation tac2expr tac2qexpr tac2types) - (libraries vernac coq-core.plugins.cc_core)) + (libraries vernac rocq-runtime.plugins.cc_core)) + +(deprecated_library_name + (old_public_name coq-core.plugins.ltac2) + (new_public_name rocq-runtime.plugins.ltac2)) (coq.pp (modules g_ltac2)) diff --git a/plugins/ltac2/g_ltac2.mlg b/plugins/ltac2/g_ltac2.mlg index 9988fd48b194..a0074144f6aa 100644 --- a/plugins/ltac2/g_ltac2.mlg +++ b/plugins/ltac2/g_ltac2.mlg @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -DECLARE PLUGIN "coq-core.plugins.ltac2" +DECLARE PLUGIN "rocq-runtime.plugins.ltac2" { @@ -973,7 +973,7 @@ let rules = [ ) ] in - Egramml.grammar_extend ~plugin_uid:("coq-core.plugins.ltac2", "g_ltac2.mlg:adhoc1") + Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ltac2", "g_ltac2.mlg:adhoc1") Procq.Constr.term (Procq.Reuse (Some"0", rules)) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 9c1ba5ef575a..7e2f147f07c6 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -19,7 +19,7 @@ open Tac2expr open Tac2entries.Pltac open Proofview.Notations -let ltac2_plugin = "coq-core.plugins.ltac2" +let ltac2_plugin = "rocq-runtime.plugins.ltac2" let constr_flags = let open Pretyping in diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml index 2d621bceba1d..5df0d176bed6 100644 --- a/plugins/ltac2/tac2entries.ml +++ b/plugins/ltac2/tac2entries.ml @@ -1238,7 +1238,7 @@ let ltac2_interp e = let tac = Tac2interp.interp Tac2interp.empty_environment e in Proofview.tclIGNORE tac -let ComTactic.Interpreter ltac2_interp = ComTactic.register_tactic_interpreter "coq-core.plugins.ltac2" ltac2_interp +let ComTactic.Interpreter ltac2_interp = ComTactic.register_tactic_interpreter "rocq-runtime.plugins.ltac2" ltac2_interp let call ~pstate g ~with_end_tac tac = let g = Option.default (Goal_select.get_default_goal_selector()) g in @@ -1283,4 +1283,4 @@ let () = Mltop.declare_cache_obj begin fun () -> ("[]", []); ("::", [GTypVar 0; GTypRef (Other t_list, [GTypVar 0])]); ]; -end "coq-core.plugins.ltac2" +end "rocq-runtime.plugins.ltac2" diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml index 156bf01494eb..1a659941b09e 100644 --- a/plugins/ltac2/tac2stdlib.ml +++ b/plugins/ltac2/tac2stdlib.ml @@ -247,7 +247,7 @@ let generalize_arg = make_to_repr to_generalize_arg open Tac2externals let define s = - define { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s } + define { mltac_plugin = "rocq-runtime.plugins.ltac2"; mltac_tactic = s } (** Tactics from Tacexpr *) diff --git a/plugins/ltac2_ltac1/dune b/plugins/ltac2_ltac1/dune index abd2ddf0748b..d87100b3bcb5 100644 --- a/plugins/ltac2_ltac1/dune +++ b/plugins/ltac2_ltac1/dune @@ -1,7 +1,11 @@ (library (name ltac2_ltac1_plugin) - (public_name coq-core.plugins.ltac2_ltac1) + (public_name rocq-runtime.plugins.ltac2_ltac1) (synopsis "Ltac2 and Ltac1 interoperability plugin") (libraries ltac_plugin ltac2_plugin)) +(deprecated_library_name + (old_public_name coq-core.plugins.ltac2_ltac1) + (new_public_name rocq-runtime.plugins.ltac2_ltac1)) + (coq.pp (modules g_ltac2_ltac1)) diff --git a/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg b/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg index 046b1ee6ee77..02567ea3ebbf 100644 --- a/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg +++ b/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -DECLARE PLUGIN "coq-core.plugins.ltac2_ltac1" +DECLARE PLUGIN "rocq-runtime.plugins.ltac2_ltac1" { diff --git a/plugins/ltac2_ltac1/tac2core_ltac1.ml b/plugins/ltac2_ltac1/tac2core_ltac1.ml index 01cd439d6e4c..216aadd307a4 100644 --- a/plugins/ltac2_ltac1/tac2core_ltac1.ml +++ b/plugins/ltac2_ltac1/tac2core_ltac1.ml @@ -20,7 +20,7 @@ open Tac2expr open Proofview.Notations open Tac2externals -let ltac2_ltac1_plugin = "coq-core.plugins.ltac2_ltac1" +let ltac2_ltac1_plugin = "rocq-runtime.plugins.ltac2_ltac1" let pname ?(plugin=ltac2_ltac1_plugin) s = { mltac_plugin = plugin; mltac_tactic = s } diff --git a/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml b/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml index bfca2ad20cad..1966512266fa 100644 --- a/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml +++ b/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml @@ -18,7 +18,7 @@ open Tac2expr open Proofview.Notations open Tac2externals -let ltac2_ltac1_plugin = "coq-core.plugins.ltac2_ltac1" +let ltac2_ltac1_plugin = "rocq-runtime.plugins.ltac2_ltac1" let pname ?(plugin=ltac2_ltac1_plugin) s = { mltac_plugin = plugin; mltac_tactic = s } diff --git a/plugins/micromega/dune b/plugins/micromega/dune index d5f5f61cdbbf..7b7df2cfe3d6 100644 --- a/plugins/micromega/dune +++ b/plugins/micromega/dune @@ -1,32 +1,44 @@ (library (name micromega_core_plugin) - (public_name coq-core.plugins.micromega_core) + (public_name rocq-runtime.plugins.micromega_core) (modules micromega numCompat mutils sos_types sos_lib sos) (synopsis "Rocq's micromega core plugin") - (libraries zarith coq-core.clib)) + (libraries zarith rocq-runtime.clib)) + +(deprecated_library_name + (old_public_name coq-core.plugins.micromega_core) + (new_public_name rocq-runtime.plugins.micromega_core)) (library (name micromega_plugin) - (public_name coq-core.plugins.micromega) + (public_name rocq-runtime.plugins.micromega) ; be careful not to link the executable to the plugin! (modules (:standard \ micromega numCompat mutils sos_types sos_lib sos csdpcert g_zify zify)) (flags :standard -open Micromega_core_plugin) (synopsis "Rocq's micromega plugin") - (libraries coq-core.plugins.ltac coq-core.plugins.micromega_core)) + (libraries rocq-runtime.plugins.ltac rocq-runtime.plugins.micromega_core)) + +(deprecated_library_name + (old_public_name coq-core.plugins.micromega) + (new_public_name rocq-runtime.plugins.micromega)) (executable (name csdpcert) (public_name csdpcert) - (package coq-core) + (package rocq-runtime) (modules csdpcert) (flags :standard -open Micromega_core_plugin) - (libraries coq-core.plugins.micromega_core)) + (libraries rocq-runtime.plugins.micromega_core)) (library (name zify_plugin) - (public_name coq-core.plugins.zify) + (public_name rocq-runtime.plugins.zify) (modules g_zify zify) (synopsis "Rocq's zify plugin") - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.zify) + (new_public_name rocq-runtime.plugins.zify)) (coq.pp (modules g_micromega g_zify)) diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg index b73c05a6a382..1f530ad038dc 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -24,7 +24,7 @@ open Tacarg } -DECLARE PLUGIN "coq-core.plugins.micromega" +DECLARE PLUGIN "rocq-runtime.plugins.micromega" TACTIC EXTEND Lra_Q | [ "xlra_Q" tactic(t) ] -> { Coq_micromega.xlra_Q (Tacinterp.tactic_of_value ist t) } diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 9b846487fc9c..e7da486cb744 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -18,7 +18,7 @@ let locality = Zify.zify_register_locality } -DECLARE PLUGIN "coq-core.plugins.zify" +DECLARE PLUGIN "rocq-runtime.plugins.zify" VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF | #[ locality ] ["Add" "Zify" "InjTyp" reference(t) ] -> { Zify.InjTable.register locality t } diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune index 4ced3d442557..1970f64c12d7 100644 --- a/plugins/nsatz/dune +++ b/plugins/nsatz/dune @@ -1,16 +1,24 @@ (library (name nsatz_core_plugin) - (public_name coq-core.plugins.nsatz_core) + (public_name rocq-runtime.plugins.nsatz_core) (synopsis "Rocq's nsatz solver plugin") (modules (:standard \ g_nsatz)) - (libraries coq-core.tactics)) + (libraries rocq-runtime.tactics)) + +(deprecated_library_name + (old_public_name coq-core.plugins.nsatz_core) + (new_public_name rocq-runtime.plugins.nsatz_core)) (library (name nsatz_plugin) - (public_name coq-core.plugins.nsatz) + (public_name rocq-runtime.plugins.nsatz) (synopsis "Rocq's nsatz solver plugin (Ltac1 syntax)") (modules g_nsatz) (flags :standard -open Nsatz_core_plugin) - (libraries coq-core.plugins.nsatz_core coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.nsatz_core rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.nsatz) + (new_public_name rocq-runtime.plugins.nsatz)) (coq.pp (modules g_nsatz)) diff --git a/plugins/nsatz/g_nsatz.mlg b/plugins/nsatz/g_nsatz.mlg index b4db0ee2a1b7..b757d6d0bc73 100644 --- a/plugins/nsatz/g_nsatz.mlg +++ b/plugins/nsatz/g_nsatz.mlg @@ -15,7 +15,7 @@ open Stdarg } -DECLARE PLUGIN "coq-core.plugins.nsatz" +DECLARE PLUGIN "rocq-runtime.plugins.nsatz" TACTIC EXTEND nsatz_compute | [ "nsatz_compute" constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) } diff --git a/plugins/ring/dune b/plugins/ring/dune index 388bd4195b66..e263d21fe8fd 100644 --- a/plugins/ring/dune +++ b/plugins/ring/dune @@ -1,7 +1,11 @@ (library (name ring_plugin) - (public_name coq-core.plugins.ring) + (public_name rocq-runtime.plugins.ring) (synopsis "Rocq's ring plugin") - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.ring) + (new_public_name rocq-runtime.plugins.ring)) (coq.pp (modules g_ring)) diff --git a/plugins/ring/g_ring.mlg b/plugins/ring/g_ring.mlg index afffc496cf42..a472fd40dbf7 100644 --- a/plugins/ring/g_ring.mlg +++ b/plugins/ring/g_ring.mlg @@ -22,7 +22,7 @@ open Pltac } -DECLARE PLUGIN "coq-core.plugins.ring" +DECLARE PLUGIN "rocq-runtime.plugins.ring" TACTIC EXTEND protect_fv | [ "protect_fv" string(map) "in" ident(id) ] -> diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index e2ce991a644d..07891c4cd538 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -144,7 +144,7 @@ let closed_term args _ = match args with let closed_term_ast = let tacname = { - mltac_plugin = "coq-core.plugins.ring"; + mltac_plugin = "rocq-runtime.plugins.ring"; mltac_tactic = "closed_term"; } in let () = Tacenv.register_ml_tactic tacname [|closed_term|] in @@ -201,7 +201,7 @@ let tactic_res = ref [||] let get_res = let open Tacexpr in - let name = { mltac_plugin = "coq-core.plugins.ring"; mltac_tactic = "get_res"; } in + let name = { mltac_plugin = "rocq-runtime.plugins.ring"; mltac_tactic = "get_res"; } in let entry = { mltac_name = name; mltac_index = 0 } in let tac args ist = let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in diff --git a/plugins/rtauto/dune b/plugins/rtauto/dune index ca4075e4c51a..79a00a53d3a4 100644 --- a/plugins/rtauto/dune +++ b/plugins/rtauto/dune @@ -1,7 +1,11 @@ (library (name rtauto_plugin) - (public_name coq-core.plugins.rtauto) + (public_name rocq-runtime.plugins.rtauto) (synopsis "Rocq's rtauto plugin") - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.rtauto) + (new_public_name rocq-runtime.plugins.rtauto)) (coq.pp (modules g_rtauto)) diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg index e84d53641b93..cafb48be27fc 100644 --- a/plugins/rtauto/g_rtauto.mlg +++ b/plugins/rtauto/g_rtauto.mlg @@ -14,7 +14,7 @@ open Ltac_plugin } -DECLARE PLUGIN "coq-core.plugins.rtauto" +DECLARE PLUGIN "rocq-runtime.plugins.rtauto" TACTIC EXTEND rtauto | [ "rtauto" ] -> { Refl_tauto.rtauto_tac } diff --git a/plugins/ssr/dune b/plugins/ssr/dune index 2cfbbc3146e6..1f549f96e374 100644 --- a/plugins/ssr/dune +++ b/plugins/ssr/dune @@ -1,9 +1,13 @@ (library (name ssreflect_plugin) - (public_name coq-core.plugins.ssreflect) + (public_name rocq-runtime.plugins.ssreflect) (synopsis "Rocq's ssreflect plugin") (modules_without_implementation ssrast) (flags :standard -open Gramlib) - (libraries coq-core.plugins.ssrmatching)) + (libraries rocq-runtime.plugins.ssrmatching)) + +(deprecated_library_name + (old_public_name coq-core.plugins.ssreflect) + (new_public_name rocq-runtime.plugins.ssreflect)) (coq.pp (modules ssrvernac ssrparser ssrtacs)) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 4498a57dbf93..e16f48d10945 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -60,12 +60,12 @@ let () = Pptactic.ssr_loaded_hook is_ssr_loaded } -DECLARE PLUGIN "coq-core.plugins.ssreflect" +DECLARE PLUGIN "rocq-runtime.plugins.ssreflect" { let ssrtac_name name = { - mltac_plugin = "coq-core.plugins.ssreflect"; + mltac_plugin = "rocq-runtime.plugins.ssreflect"; mltac_tactic = "ssr" ^ name; } @@ -105,7 +105,7 @@ let register_ssrtac name f prods = } in let obj () = Lib.add_leaf (inSsrGrammar (key, body, parule)) in - Mltop.declare_cache_obj obj "coq-core.plugins.ssreflect"; + Mltop.declare_cache_obj obj "rocq-runtime.plugins.ssreflect"; key let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v @@ -117,7 +117,7 @@ let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = ref (Procq.get_keyword_state ()) ;; -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> frozen_lexer := Procq.get_keyword_state ()) let tacltop = (LevelLe 5) @@ -1745,7 +1745,7 @@ type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> Procq.set_keyword_state !frozen_lexer) ;; module Internal = struct diff --git a/plugins/ssr/ssrtacs.mlg b/plugins/ssr/ssrtacs.mlg index ce17fa50da1d..263b94228d62 100644 --- a/plugins/ssr/ssrtacs.mlg +++ b/plugins/ssr/ssrtacs.mlg @@ -47,13 +47,13 @@ open Ssrmatching_plugin.G_ssrmatching } -DECLARE PLUGIN "coq-core.plugins.ssreflect" +DECLARE PLUGIN "rocq-runtime.plugins.ssreflect" { (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = ref (Procq.get_keyword_state ()) ;; -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> frozen_lexer := Procq.get_keyword_state ()) } @@ -1057,7 +1057,7 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> Procq.set_keyword_state !frozen_lexer) ;; } diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 3d6bfa2ad846..a0e3add36c11 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -33,14 +33,14 @@ open Ssrcommon } -DECLARE PLUGIN "coq-core.plugins.ssreflect" +DECLARE PLUGIN "rocq-runtime.plugins.ssreflect" { (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = ref (Procq.get_keyword_state ()) ;; -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> frozen_lexer := Procq.get_keyword_state ()) (* global syntactic changes and vernacular commands *) @@ -361,7 +361,7 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> Procq.set_keyword_state !frozen_lexer) ;; } diff --git a/plugins/ssrmatching/dune b/plugins/ssrmatching/dune index 8bfe21216211..a3eea1d4799d 100644 --- a/plugins/ssrmatching/dune +++ b/plugins/ssrmatching/dune @@ -1,7 +1,11 @@ (library (name ssrmatching_plugin) - (public_name coq-core.plugins.ssrmatching) + (public_name rocq-runtime.plugins.ssrmatching) (synopsis "Rocq ssrmatching plugin") - (libraries coq-core.plugins.ltac)) + (libraries rocq-runtime.plugins.ltac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.ssrmatching) + (new_public_name rocq-runtime.plugins.ssrmatching)) (coq.pp (modules g_ssrmatching)) diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 58ecb5b55891..cb38f63eb202 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -20,12 +20,12 @@ open Ssrmatching.Internal (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = ref (Procq.get_keyword_state ()) ;; -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> frozen_lexer := Procq.get_keyword_state ()) } -DECLARE PLUGIN "coq-core.plugins.ssrmatching" +DECLARE PLUGIN "rocq-runtime.plugins.ssrmatching" { @@ -118,7 +118,7 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () -> +let () = Mltop.add_init_function "rocq-runtime.plugins.ssreflect" (fun () -> Procq.set_keyword_state !frozen_lexer) ;; } diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 67c5f7b78c72..79092e176d4b 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1386,14 +1386,14 @@ let () = let v = Id.Map.find (Names.Id.of_string "pattern") ist.lfun in Value.cast (topwit wit_ssrpatternarg) v in ssrpatterntac ist arg in - let name = { mltac_plugin = "coq-core.plugins.ssrmatching"; mltac_tactic = "ssrpattern"; } in + let name = { mltac_plugin = "rocq-runtime.plugins.ssrmatching"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = CAst.make (TacFun ([Name (Id.of_string "pattern")], CAst.make (TacML ({ mltac_name = name; mltac_index = 0 }, [])))) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in - Mltop.declare_cache_obj obj "coq-core.plugins.ssrmatching" + Mltop.declare_cache_obj obj "rocq-runtime.plugins.ssrmatching" let ssrinstancesof arg = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/syntax/dune b/plugins/syntax/dune index c798acb35926..72959e88cadf 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -1,8 +1,12 @@ (library (name number_string_notation_plugin) - (public_name coq-core.plugins.number_string_notation) + (public_name rocq-runtime.plugins.number_string_notation) (synopsis "Rocq number and string notation plugin") (modules g_number_string number_string) - (libraries coq-core.vernac)) + (libraries rocq-runtime.vernac)) + +(deprecated_library_name + (old_public_name coq-core.plugins.number_string_notation) + (new_public_name rocq-runtime.plugins.number_string_notation)) (coq.pp (modules g_number_string)) diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg index 4e7eaea45ebc..a492853cbc7e 100644 --- a/plugins/syntax/g_number_string.mlg +++ b/plugins/syntax/g_number_string.mlg @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -DECLARE PLUGIN "coq-core.plugins.number_string_notation" +DECLARE PLUGIN "rocq-runtime.plugins.number_string_notation" { diff --git a/pretyping/dune b/pretyping/dune index ffad4d2daac0..b9f9d9bf7506 100644 --- a/pretyping/dune +++ b/pretyping/dune @@ -1,7 +1,11 @@ (library (name pretyping) (synopsis "Coq's Type Inference Component (Pretyper)") - (public_name coq-core.pretyping) + (public_name rocq-runtime.pretyping) (wrapped false) (modules_without_implementation locus pattern glob_term ltac_pretype) (libraries engine)) + +(deprecated_library_name + (old_public_name coq-core.pretyping) + (new_public_name rocq-runtime.pretyping)) diff --git a/printing/dune b/printing/dune index a24a7535ebbf..9f5c1e704a62 100644 --- a/printing/dune +++ b/printing/dune @@ -1,6 +1,10 @@ (library (name printing) (synopsis "Coq's Term Pretty Printing Library") - (public_name coq-core.printing) + (public_name rocq-runtime.printing) (wrapped false) (libraries parsing proofs)) + +(deprecated_library_name + (old_public_name coq-core.printing) + (new_public_name rocq-runtime.printing)) diff --git a/proofs/dune b/proofs/dune index 7a49558b6bc7..e8d6b8d5fab0 100644 --- a/proofs/dune +++ b/proofs/dune @@ -1,7 +1,11 @@ (library (name proofs) (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure") - (public_name coq-core.proofs) + (public_name rocq-runtime.proofs) (wrapped false) (modules_without_implementation tactypes) (libraries pretyping)) + +(deprecated_library_name + (old_public_name coq-core.proofs) + (new_public_name rocq-runtime.proofs)) diff --git a/rocq-core.opam b/rocq-core.opam index ef61e71a34f8..9c1332abad91 100644 --- a/rocq-core.opam +++ b/rocq-core.opam @@ -25,14 +25,14 @@ doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" depends: [ "dune" {>= "3.8"} - "coq-core" {= version} + "rocq-runtime" {= version} "odoc" {with-doc} ] depopts: ["coq-native"] dev-repo: "git+https://github.com/coq/coq.git" build: [ ["dune" "subst"] {dev} - # We tell dunestrap to use coq-config from coq-core + # We tell dunestrap to use coq-config from rocq-runtime [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"] [ "dune" diff --git a/rocq-core.opam.template b/rocq-core.opam.template index d16674c66a10..e67a6ea385ec 100644 --- a/rocq-core.opam.template +++ b/rocq-core.opam.template @@ -1,6 +1,6 @@ build: [ ["dune" "subst"] {dev} - # We tell dunestrap to use coq-config from coq-core + # We tell dunestrap to use coq-config from rocq-runtime [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"] [ "dune" diff --git a/rocq-runtime.opam b/rocq-runtime.opam new file mode 100644 index 000000000000..8dea4a73a6dc --- /dev/null +++ b/rocq-runtime.opam @@ -0,0 +1,60 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +synopsis: "The Coq Proof Assistant -- Core Binaries and Tools" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq core binaries, plugins, and tools, but +not the vernacular standard library. + +Note that in this setup, Coq needs to be started with the -boot and +-noinit options, as will otherwise fail to find the regular Coq +prelude, now living in the rocq-core package.""" +maintainer: ["The Coq development team "] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "3.8"} + "ocaml" {>= "4.09.0"} + "ocamlfind" {>= "1.8.1"} + "zarith" {>= "1.11"} + "conf-linux-libc-dev" {os = "linux"} + "odoc" {with-doc} +] +depopts: ["coq-native" "memprof-limits" "memtrace"] +dev-repo: "git+https://github.com/coq/coq.git" +build: [ + ["dune" "subst"] {dev} + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] diff --git a/coq-core.opam.template b/rocq-runtime.opam.template similarity index 100% rename from coq-core.opam.template rename to rocq-runtime.opam.template diff --git a/stdlib/dune-project b/stdlib/dune-project index 6c06a6cb543d..0a1760cae7db 100644 --- a/stdlib/dune-project +++ b/stdlib/dune-project @@ -24,7 +24,7 @@ (package (name coq-stdlib) (depends - coq-core + coq-core ; dune coq mode needs the coq compat binaries (rocq-core (= :version))) (depopts coq-native) (synopsis "The Coq Proof Assistant -- Standard Library") diff --git a/stdlib/test-suite/micromega/witness_tactics.v b/stdlib/test-suite/micromega/witness_tactics.v index c63c08dcfe8f..c4c12066e594 100644 --- a/stdlib/test-suite/micromega/witness_tactics.v +++ b/stdlib/test-suite/micromega/witness_tactics.v @@ -2,7 +2,7 @@ From Stdlib Require Import ZArith QArith. From Stdlib.micromega Require Import RingMicromega EnvRing Tauto. From Stdlib.micromega Require Import ZMicromega QMicromega. -Declare ML Module "coq-core.plugins.micromega". +Declare ML Module "rocq-runtime.plugins.micromega". Goal True. Proof. diff --git a/stdlib/theories/btauto/Btauto.v b/stdlib/theories/btauto/Btauto.v index b1345cd65535..16d92e1cf18c 100644 --- a/stdlib/theories/btauto/Btauto.v +++ b/stdlib/theories/btauto/Btauto.v @@ -1,3 +1,3 @@ Require Import Algebra Reflect. -Declare ML Module "coq-core.plugins.btauto". +Declare ML Module "rocq-runtime.plugins.btauto". diff --git a/stdlib/theories/funind/FunInd.v b/stdlib/theories/funind/FunInd.v index c21b8ced339a..01ccd90cec9e 100644 --- a/stdlib/theories/funind/FunInd.v +++ b/stdlib/theories/funind/FunInd.v @@ -9,4 +9,4 @@ (************************************************************************) Require Stdlib.extraction.Extraction. -Declare ML Module "coq-core.plugins.funind". +Declare ML Module "rocq-runtime.plugins.funind". diff --git a/stdlib/theories/micromega/Lia.v b/stdlib/theories/micromega/Lia.v index 22378152a441..89aa88b4de08 100644 --- a/stdlib/theories/micromega/Lia.v +++ b/stdlib/theories/micromega/Lia.v @@ -17,8 +17,8 @@ Require Import ZMicromega RingMicromega VarMap DeclConstant. Require Import BinNums. Require Stdlib.micromega.Tauto. -Declare ML Module "coq-core.plugins.micromega_core". -Declare ML Module "coq-core.plugins.micromega". +Declare ML Module "rocq-runtime.plugins.micromega_core". +Declare ML Module "rocq-runtime.plugins.micromega". Ltac zchecker := let __wit := fresh "__wit" in diff --git a/stdlib/theories/micromega/Lqa.v b/stdlib/theories/micromega/Lqa.v index 41b96dd4b9fe..a973d59788fd 100644 --- a/stdlib/theories/micromega/Lqa.v +++ b/stdlib/theories/micromega/Lqa.v @@ -20,8 +20,8 @@ Require Import RingMicromega. Require Import VarMap. Require Import DeclConstant. Require Stdlib.micromega.Tauto. -Declare ML Module "coq-core.plugins.micromega_core". -Declare ML Module "coq-core.plugins.micromega". +Declare ML Module "rocq-runtime.plugins.micromega_core". +Declare ML Module "rocq-runtime.plugins.micromega". Ltac rchange := let __wit := fresh "__wit" in diff --git a/stdlib/theories/micromega/Lra.v b/stdlib/theories/micromega/Lra.v index 06cd9c992bfa..4a27d90f5971 100644 --- a/stdlib/theories/micromega/Lra.v +++ b/stdlib/theories/micromega/Lra.v @@ -22,7 +22,7 @@ Require Import VarMap. Require Stdlib.micromega.Tauto. Require Import Rregisternames. -Declare ML Module "coq-core.plugins.micromega". +Declare ML Module "rocq-runtime.plugins.micromega". Ltac rchange := let __wit := fresh "__wit" in diff --git a/stdlib/theories/micromega/Psatz.v b/stdlib/theories/micromega/Psatz.v index fa120e25b461..324ab2c4983b 100644 --- a/stdlib/theories/micromega/Psatz.v +++ b/stdlib/theories/micromega/Psatz.v @@ -27,7 +27,7 @@ Require Lia. Require Lra. Require Lqa. -Declare ML Module "coq-core.plugins.micromega". +Declare ML Module "rocq-runtime.plugins.micromega". Ltac lia := Lia.lia. diff --git a/stdlib/theories/micromega/Zify.v b/stdlib/theories/micromega/Zify.v index 0ee62281340a..8d0413296594 100644 --- a/stdlib/theories/micromega/Zify.v +++ b/stdlib/theories/micromega/Zify.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import ZifyClasses ZifyInst. -Declare ML Module "coq-core.plugins.zify". +Declare ML Module "rocq-runtime.plugins.zify". (** [zify_pre_hook] and [zify_post_hook] are there to be redefined. *) Ltac zify_pre_hook := idtac. diff --git a/stdlib/theories/micromega/ZifyInst.v b/stdlib/theories/micromega/ZifyInst.v index 706a703201a4..d1561b3f60e9 100644 --- a/stdlib/theories/micromega/ZifyInst.v +++ b/stdlib/theories/micromega/ZifyInst.v @@ -14,7 +14,7 @@ Require Import Arith BinInt BinNat Znat Nnat. Require Import ZifyClasses. -Declare ML Module "coq-core.plugins.zify". +Declare ML Module "rocq-runtime.plugins.zify". Local Open Scope Z_scope. Ltac refl := diff --git a/stdlib/theories/nsatz/NsatzTactic.v b/stdlib/theories/nsatz/NsatzTactic.v index 14502130ea67..176f674da4e9 100644 --- a/stdlib/theories/nsatz/NsatzTactic.v +++ b/stdlib/theories/nsatz/NsatzTactic.v @@ -32,8 +32,8 @@ Require Export Integral_domain. Require Import ZArith. Require Import Lia. -Declare ML Module "coq-core.plugins.nsatz_core". -Declare ML Module "coq-core.plugins.nsatz". +Declare ML Module "rocq-runtime.plugins.nsatz_core". +Declare ML Module "rocq-runtime.plugins.nsatz". Section nsatz1. diff --git a/stdlib/theories/rtauto/Rtauto.v b/stdlib/theories/rtauto/Rtauto.v index 4d642a4f4736..60d1ec1efb99 100644 --- a/stdlib/theories/rtauto/Rtauto.v +++ b/stdlib/theories/rtauto/Rtauto.v @@ -13,7 +13,7 @@ Require Export List. Require Export Bintree. Require Import Bool BinPos. -Declare ML Module "coq-core.plugins.rtauto". +Declare ML Module "rocq-runtime.plugins.rtauto". Ltac clean:=try (simpl;congruence). diff --git a/stdlib/theories/setoid_ring/Ring_base.v b/stdlib/theories/setoid_ring/Ring_base.v index 68077020eced..9b0a6059b2f7 100644 --- a/stdlib/theories/setoid_ring/Ring_base.v +++ b/stdlib/theories/setoid_ring/Ring_base.v @@ -12,7 +12,7 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Declare ML Module "coq-core.plugins.ring". +Declare ML Module "rocq-runtime.plugins.ring". Require Export Ring_theory. Require Export Ring_tac. Require Import InitialRing. diff --git a/stdlib/theories/setoid_ring/Ring_tac.v b/stdlib/theories/setoid_ring/Ring_tac.v index 131ccad0c419..605e901d3720 100644 --- a/stdlib/theories/setoid_ring/Ring_tac.v +++ b/stdlib/theories/setoid_ring/Ring_tac.v @@ -15,7 +15,7 @@ Require Import Ring_polynom. Require Import BinList. Require Export ListTactics. Require Import InitialRing. -Declare ML Module "coq-core.plugins.ring". +Declare ML Module "rocq-runtime.plugins.ring". (* adds a definition t' on the normal form of t and an hypothesis id stating that t = t' (tries to produces a proof as small as possible) *) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 27a17e8fcfe8..3ecfc3041718 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -110,7 +110,7 @@ module Make(T : Task) () = struct let uid = ref 0 let get_toplevel_path top = - let dir = Findlib.package_directory "coq-core" in + let dir = Findlib.package_directory "rocq-runtime" in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in Filename.concat dir (top^exe) diff --git a/stm/dune b/stm/dune index 1aa5523f3415..4b3ea5c9b924 100644 --- a/stm/dune +++ b/stm/dune @@ -1,8 +1,12 @@ (library (name stm) (synopsis "Coq's Document Manager and Proof Checking Scheduler") - (public_name coq-core.stm) + (public_name rocq-runtime.stm) (wrapped false) ; until ocaml/dune#4892 fixed ; (private_modules dag proofBlockDelimiter tQueue vcs workerPool) (libraries sysinit coqworkmgrlib)) + +(deprecated_library_name + (old_public_name coq-core.stm) + (new_public_name rocq-runtime.stm)) diff --git a/stm/stm.ml b/stm/stm.ml index 13e0322a9ed5..647149234af9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -130,7 +130,7 @@ let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr (* Commands piercing opaque (probably should be using the vernactypes system instead) *) let may_pierce_opaque = function | VernacSynPure (VernacPrint _) -> true - | VernacSynterp (VernacExtend ({ ext_plugin = "coq-core.plugins.extraction" }, _)) -> true + | VernacSynterp (VernacExtend ({ ext_plugin = "rocq-runtime.plugins.extraction" }, _)) -> true | _ -> false type depth = int diff --git a/sysinit/dune b/sysinit/dune index 13b5730abace..cca1b0f0488a 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -1,16 +1,24 @@ (library (name coqargs) - (public_name coq-core.coqargs) + (public_name rocq-runtime.coqargs) (synopsis "Coq command line argument parsing") (modules coqargs) (wrapped false) - ; don't depend on coq-core.lib -> impossible to imperatively set random flags - (libraries coq-core.config coq-core.clib)) + ; don't depend on rocq-runtime.lib -> impossible to imperatively set random flags + (libraries rocq-runtime.config rocq-runtime.clib)) + +(deprecated_library_name + (old_public_name coq-core.coqargs) + (new_public_name rocq-runtime.coqargs)) (library (name sysinit) - (public_name coq-core.sysinit) + (public_name rocq-runtime.sysinit) (synopsis "Coq's initialization") (wrapped false) (modules :standard \ coqargs) - (libraries coq-core.boot coq-core.vernac coqargs findlib)) + (libraries rocq-runtime.boot rocq-runtime.vernac coqargs findlib)) + +(deprecated_library_name + (old_public_name coq-core.sysinit) + (new_public_name rocq-runtime.sysinit)) diff --git a/tactics/dune b/tactics/dune index afcb8fcf3a5f..6a6bb32568df 100644 --- a/tactics/dune +++ b/tactics/dune @@ -1,9 +1,13 @@ (library (name tactics) (synopsis "Coq's Core Tactics [ML implementation]") - (public_name coq-core.tactics) + (public_name rocq-runtime.tactics) (wrapped false) (modules_without_implementation genredexpr) ; until ocaml/dune#4892 fixed ; (private_modules btermdn dn) (libraries printing)) + +(deprecated_library_name + (old_public_name coq-core.tactics) + (new_public_name rocq-runtime.tactics)) diff --git a/test-suite/Makefile b/test-suite/Makefile index 0d495013c393..fc546e6b2831 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -334,7 +334,7 @@ unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -w -29 -linkpkg -package coq-core.toplevel,ounit2 \ + $(HIDE)$(OCAMLBEST) -w -29 -linkpkg -package rocq-runtime.toplevel,ounit2 \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)$(call WITH_TIMER,$@,./$<.test) $(HIDE)$(call REPORT_TIMER,$@) diff --git a/test-suite/bugs/bug_17069_1.v b/test-suite/bugs/bug_17069_1.v index 4e0c896334fe..ebe594cd890b 100644 --- a/test-suite/bugs/bug_17069_1.v +++ b/test-suite/bugs/bug_17069_1.v @@ -1,15 +1,15 @@ (* -*- coq-prog-args: ("-async-proofs-cache" "force"); -*- *) -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". Reset Initial. diff --git a/test-suite/bugs/bug_17687.v b/test-suite/bugs/bug_17687.v index f4289946659e..ade519c33d3b 100644 --- a/test-suite/bugs/bug_17687.v +++ b/test-suite/bugs/bug_17687.v @@ -1,6 +1,6 @@ (* -*- coq-prog-args: ("-noinit"); -*- *) -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". Global Set Default Proof Mode "Classic". Inductive paths {A : Type} (a : A) : forall _:A, Type := idpath : paths a a. diff --git a/test-suite/bugs/bug_3612.v b/test-suite/bugs/bug_3612.v index 3c852aa09040..d793962d2396 100644 --- a/test-suite/bugs/bug_3612.v +++ b/test-suite/bugs/bug_3612.v @@ -38,7 +38,7 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". Set Default Proof Mode "Classic". diff --git a/test-suite/bugs/bug_3649.v b/test-suite/bugs/bug_3649.v index f219ea524424..f811c196e5ba 100644 --- a/test-suite/bugs/bug_3649.v +++ b/test-suite/bugs/bug_3649.v @@ -2,7 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). diff --git a/test-suite/bugs/bug_4121.v b/test-suite/bugs/bug_4121.v index 8ca498672048..e742d22df3ea 100644 --- a/test-suite/bugs/bug_4121.v +++ b/test-suite/bugs/bug_4121.v @@ -4,7 +4,7 @@ Unset Strict Universe Declaration. (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". Set Universe Polymorphism. Class Contr_internal (A : Type) := BuildContr { center : A }. diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh index d7514586b567..89a4c5976f9a 100755 --- a/test-suite/coq-makefile/findlib-package-unpacked/run.sh +++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh @@ -2,7 +2,7 @@ . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib -sed -i.old 's/coq-core.plugins.ltac/coq-core.plugins.ltac,foo/' src/META.coq-test-suite +sed -i.old 's/rocq-runtime.plugins.ltac/rocq-runtime.plugins.ltac,foo/' src/META.coq-test-suite echo "let () = Foolib.foo ();;" >> src/test_aux.ml if which cygpath 2>/dev/null; then diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh index e7208537313b..70d38dc1f426 100755 --- a/test-suite/coq-makefile/findlib-package/run.sh +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -2,7 +2,7 @@ . ../template/init.sh -sed -i.old 's/coq-core.plugins.ltac/coq-core.plugins.ltac,foo/' src/META.coq-test-suite +sed -i.old 's/rocq-runtime.plugins.ltac/rocq-runtime.plugins.ltac,foo/' src/META.coq-test-suite echo "let () = Foolib.foo ();;" >> src/test_aux.ml if which cygpath 2>/dev/null; then diff --git a/test-suite/coq-makefile/template/src/META.coq-test-suite b/test-suite/coq-makefile/template/src/META.coq-test-suite index aecb90b755e3..f71354ad26f8 100644 --- a/test-suite/coq-makefile/template/src/META.coq-test-suite +++ b/test-suite/coq-makefile/template/src/META.coq-test-suite @@ -2,7 +2,7 @@ package "test" ( directory = "." version = "dev" description = "A test plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "test_plugin.cma" archive(native) = "test_plugin.cmxa" plugin(byte) = "test_plugin.cma" diff --git a/test-suite/dune b/test-suite/dune index 3bb43fa464bf..7327e80185b1 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -24,6 +24,7 @@ ; For the changelog test ../config/coq_config.py (source_tree doc/changelog) + (package rocq-runtime) (package coq-core) (package rocq-core) ; For fake_ide diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh index f0f105dbf113..7b5751623b13 100755 --- a/test-suite/misc/coq_environment.sh +++ b/test-suite/misc/coq_environment.sh @@ -21,7 +21,7 @@ EOT cp $BIN/coqc . cp $BIN/coq_makefile . mkdir -p overridden/tools/ -cp $COQLIB/../coq-core/tools/CoqMakefile.in overridden/tools/ +cp $COQLIB/../rocq-runtime/tools/CoqMakefile.in overridden/tools/ unset COQLIB N=`./coqc -config | grep COQLIB | grep /overridden | wc -l` diff --git a/test-suite/misc/non-marshalable-state/src/META.coq-test-suite b/test-suite/misc/non-marshalable-state/src/META.coq-test-suite index 27f1e81617da..4a659163c1e8 100644 --- a/test-suite/misc/non-marshalable-state/src/META.coq-test-suite +++ b/test-suite/misc/non-marshalable-state/src/META.coq-test-suite @@ -2,7 +2,7 @@ package "evil" ( directory = "." version = "dev" description = "An evil test plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "evil_plugin.cma" archive(native) = "evil_plugin.cmxa" plugin(byte) = "evil_plugin.cma" @@ -12,7 +12,7 @@ package "good" ( directory = "." version = "dev" description = "A good test plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "good_plugin.cma" archive(native) = "good_plugin.cmxa" plugin(byte) = "good_plugin.cma" diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg index f4f278f37cec..c423662c3fc2 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evil.mlg +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -3,7 +3,7 @@ open Stdarg open EvilImpl } -DECLARE PLUGIN "coq-core.plugins.evil" +DECLARE PLUGIN "rocq-runtime.plugins.evil" VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF | [ "Evil" ident(x) ident(y) ] -> { evil x y } diff --git a/test-suite/misc/quotation_token/META.coq-test-suite b/test-suite/misc/quotation_token/META.coq-test-suite index 1429f6cd5c2d..4572453e8057 100644 --- a/test-suite/misc/quotation_token/META.coq-test-suite +++ b/test-suite/misc/quotation_token/META.coq-test-suite @@ -2,7 +2,7 @@ package "quotation" ( directory = "src" version = "dev" description = "A quotation test plugin" - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "quotation_plugin.cma" archive(native) = "quotation_plugin.cmxa" plugin(byte) = "quotation_plugin.cma" diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg index 79c7e08dacc4..599d771175af 100644 --- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -1,4 +1,4 @@ -DECLARE PLUGIN "coq-core.plugins.evil" +DECLARE PLUGIN "rocq-runtime.plugins.evil" { open Ltac_plugin diff --git a/test-suite/output/bug_17155.out b/test-suite/output/bug_17155.out index 61fb63c8838f..825378f501a4 100644 --- a/test-suite/output/bug_17155.out +++ b/test-suite/output/bug_17155.out @@ -7,7 +7,7 @@ Uncaught Ltac2 exception: Invalid_argument None Backtrace: Call M.g Call bug_17155.M.f (* local *) -Prim +Prim Ltac2 M.g : unit -> 'a M.g := fun _ => bug_17155.M.f (* local *) () diff --git a/test-suite/output/ltac2_anomaly_backtrace.out b/test-suite/output/ltac2_anomaly_backtrace.out index 1c90cbc29cad..d6ce5c683584 100644 --- a/test-suite/output/ltac2_anomaly_backtrace.out +++ b/test-suite/output/ltac2_anomaly_backtrace.out @@ -3,7 +3,7 @@ Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. Backtrace: Call foo -Prim +Prim diff --git a/test-suite/output/ltac2_bt.out b/test-suite/output/ltac2_bt.out index b9942225fd67..fa6ade7ab2d2 100644 --- a/test-suite/output/ltac2_bt.out +++ b/test-suite/output/ltac2_bt.out @@ -2,31 +2,31 @@ File "./output/ltac2_bt.v", line 8, characters 2-48: The command has indeed failed with message: Uncaught Ltac2 exception: Invalid_argument None Backtrace: -Prim +Prim Call {Control.zero e} -Prim +Prim File "./output/ltac2_bt.v", line 9, characters 2-49: The command has indeed failed with message: Uncaught Ltac2 exception: Invalid_argument None Backtrace: -Prim +Prim Call {Control.throw e} -Prim +Prim File "./output/ltac2_bt.v", line 10, characters 2-60: The command has indeed failed with message: Uncaught Ltac2 exception: Invalid_argument None Backtrace: -Prim +Prim Call f -Prim +Prim File "./output/ltac2_bt.v", line 11, characters 2-61: The command has indeed failed with message: Uncaught Ltac2 exception: Invalid_argument None Backtrace: -Prim +Prim Call f -Prim +Prim diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v index 887f8524781b..c3b15bcaa1f9 100644 --- a/test-suite/output/ltac2_deprecated.v +++ b/test-suite/output/ltac2_deprecated.v @@ -7,7 +7,7 @@ Ltac2 foo := (). Ltac2 Notation bar := (). #[deprecated(note="test_external")] -Ltac2 @ external qux : 'a array -> int := "coq-core.plugins.ltac2" "array_length". +Ltac2 @ external qux : 'a array -> int := "rocq-runtime.plugins.ltac2" "array_length". (* Randomly picked external function *) Ltac2 Eval foo. diff --git a/test-suite/output/ltac2_printabout.out b/test-suite/output/ltac2_printabout.out index a09eceed53a6..860a185a6dee 100644 --- a/test-suite/output/ltac2_printabout.out +++ b/test-suite/output/ltac2_printabout.out @@ -2,7 +2,7 @@ fst : 'a * 'b -> 'a snd : 'b * 'a -> 'a type : constr -> constr Ltac2 type : constr -> constr - type := @external "coq-core.plugins.ltac2" "constr_type" + type := @external "rocq-runtime.plugins.ltac2" "constr_type" Ltac2 ltac2_printabout.type Ltac2 type : constr -> constr None : 'a option diff --git a/test-suite/output/ltac2_printabout.v b/test-suite/output/ltac2_printabout.v index c27c72ffe126..5f472db1bb69 100644 --- a/test-suite/output/ltac2_printabout.v +++ b/test-suite/output/ltac2_printabout.v @@ -1,6 +1,6 @@ Require Import Ltac2.Init. -Ltac2 @ external type : constr -> constr := "coq-core.plugins.ltac2" "constr_type". +Ltac2 @ external type : constr -> constr := "rocq-runtime.plugins.ltac2" "constr_type". Print Ltac2 Signatures. diff --git a/test-suite/precomputed-time-tests/no-output-sync/time-of-build.log.in b/test-suite/precomputed-time-tests/no-output-sync/time-of-build.log.in index 47b97ec73921..c97a8d20f2c6 100644 --- a/test-suite/precomputed-time-tests/no-output-sync/time-of-build.log.in +++ b/test-suite/precomputed-time-tests/no-output-sync/time-of-build.log.in @@ -753,7 +753,7 @@ CONTRIBUTING.md CREDITS INSTALL.md LICENSE -META.coq-core.in +META.rocq-runtime.in Makefile Makefile.build Makefile.checker diff --git a/test-suite/precomputed-time-tests/template/init.sh b/test-suite/precomputed-time-tests/template/init.sh index c79dcd0bbe3a..7a14ea276820 100644 --- a/test-suite/precomputed-time-tests/template/init.sh +++ b/test-suite/precomputed-time-tests/template/init.sh @@ -8,7 +8,7 @@ export PATH="$COQBIN:$PATH" export LC_ALL=C # tools -TTOOLSDIR="$COQPREFIX/lib/coq-core/tools" +TTOOLSDIR="$COQPREFIX/lib/rocq-runtime/tools" export make_both_time_files="$TTOOLSDIR"/make-both-time-files.py export make_one_time_file="$TTOOLSDIR"/make-one-time-file.py diff --git a/test-suite/prerequisite/funind.v b/test-suite/prerequisite/funind.v index ac78cfb053ff..74e06e429bab 100644 --- a/test-suite/prerequisite/funind.v +++ b/test-suite/prerequisite/funind.v @@ -9,4 +9,4 @@ (************************************************************************) From Corelib Require Extraction. -Declare ML Module "funind_plugin:coq-core.plugins.funind". +Declare ML Module "rocq-runtime.plugins.funind". diff --git a/test-suite/stm/classify_set_proof_mode_9093.v b/test-suite/stm/classify_set_proof_mode_9093.v index bd051ffc0afb..9a6a55f40bc7 100644 --- a/test-suite/stm/classify_set_proof_mode_9093.v +++ b/test-suite/stm/classify_set_proof_mode_9093.v @@ -1,6 +1,6 @@ (* -*- coq-prog-args: ("-async-proofs" "on" "-noinit"); -*- *) -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". Set Default Proof Mode "Classic". diff --git a/test-suite/success/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v index 0feba189cc31..4ca07528d5cc 100644 --- a/test-suite/success/Discriminate_HoTT.v +++ b/test-suite/success/Discriminate_HoTT.v @@ -9,7 +9,7 @@ Unset Elimination Schemes. Set Universe Polymorphism. -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". Global Set Default Proof Mode "Classic". diff --git a/test-suite/tools/dune b/test-suite/tools/dune index b701a05a8958..c582bfcad54b 100644 --- a/test-suite/tools/dune +++ b/test-suite/tools/dune @@ -1,3 +1,3 @@ (executable (name coq_config_to_make) - (libraries coq-core.config)) + (libraries rocq-runtime.config)) diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index ae451619c56c..10e95d555ae5 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -16,7 +16,7 @@ Require Import Corelib.Init.Logic. Require Import Corelib.Init.Specif. Require Corelib.Init.Nat. -Declare ML Module "coq-core.plugins.number_string_notation". +Declare ML Module "rocq-runtime.plugins.number_string_notation". (** We define an inductive for use with the [String Notation] command which contains all ascii characters. We use 256 constructors for diff --git a/theories/Init/Ltac.v b/theories/Init/Ltac.v index 1f0d23d66256..7a3832568297 100644 --- a/theories/Init/Ltac.v +++ b/theories/Init/Ltac.v @@ -8,6 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Declare ML Module "coq-core.plugins.ltac". +Declare ML Module "rocq-runtime.plugins.ltac". #[export] Set Default Proof Mode "Classic". diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 07fef7dd255c..2c30b7d3f277 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -27,10 +27,10 @@ Require Export Corelib.Init.Sumbool. - ltac_plugin (in Ltac) - tauto_plugin (in Tauto). *) -Declare ML Module "coq-core.plugins.cc_core". -Declare ML Module "coq-core.plugins.cc". -Declare ML Module "coq-core.plugins.firstorder_core". -Declare ML Module "coq-core.plugins.firstorder". +Declare ML Module "rocq-runtime.plugins.cc_core". +Declare ML Module "rocq-runtime.plugins.cc". +Declare ML Module "rocq-runtime.plugins.firstorder_core". +Declare ML Module "rocq-runtime.plugins.firstorder". (* Parsing / printing of hexadecimal numbers *) Arguments Nat.of_hex_uint d%_hex_uint_scope. diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v index 83676041f4a1..c13813b3b90f 100644 --- a/theories/Init/Tauto.v +++ b/theories/Init/Tauto.v @@ -15,7 +15,7 @@ Require Import Ltac. Require Import Datatypes. Require Import Logic. -Declare ML Module "coq-core.plugins.tauto". +Declare ML Module "rocq-runtime.plugins.tauto". Local Ltac not_dep_intros := repeat match goal with diff --git a/theories/derive/Derive.v b/theories/derive/Derive.v index 4f7da157f64c..ef7f93c0a092 100644 --- a/theories/derive/Derive.v +++ b/theories/derive/Derive.v @@ -1 +1 @@ -Declare ML Module "coq-core.plugins.derive". +Declare ML Module "rocq-runtime.plugins.derive". diff --git a/theories/dune.disabled b/theories/dune.disabled index 163878cc725b..37e83bded984 100644 --- a/theories/dune.disabled +++ b/theories/dune.disabled @@ -7,27 +7,27 @@ ; (mode native) (boot) (plugins - coq-core.plugins.ltac - coq-core.plugins.tauto + rocq-runtime.plugins.ltac + rocq-runtime.plugins.tauto - coq-core.plugins.cc - coq-core.plugins.firstorder + rocq-runtime.plugins.cc + rocq-runtime.plugins.firstorder - coq-core.plugins.number_string_notation + rocq-runtime.plugins.number_string_notation - coq-core.plugins.btauto - coq-core.plugins.rtauto + rocq-runtime.plugins.btauto + rocq-runtime.plugins.rtauto - coq-core.plugins.ring - coq-core.plugins.nsatz + rocq-runtime.plugins.ring + rocq-runtime.plugins.nsatz - coq-core.plugins.zify - coq-core.plugins.micromega + rocq-runtime.plugins.zify + rocq-runtime.plugins.micromega - coq-core.plugins.funind + rocq-runtime.plugins.funind - coq-core.plugins.ssreflect - coq-core.plugins.derive)) + rocq-runtime.plugins.ssreflect + rocq-runtime.plugins.derive)) (include_subdirs qualified) diff --git a/theories/extraction/Extraction.v b/theories/extraction/Extraction.v index 4093152be6f6..6aaf7bcb2bcd 100644 --- a/theories/extraction/Extraction.v +++ b/theories/extraction/Extraction.v @@ -8,4 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Declare ML Module "coq-core.plugins.extraction". +Declare ML Module "rocq-runtime.plugins.extraction". diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index 22d7c5b41619..0d600d3f02a6 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -13,7 +13,7 @@ (** ## **) Require Import ssrmatching. -Declare ML Module "coq-core.plugins.ssreflect". +Declare ML Module "rocq-runtime.plugins.ssreflect". (** This file is the Gallina part of the ssreflect plugin implementation. diff --git a/theories/ssrmatching/ssrmatching.v b/theories/ssrmatching/ssrmatching.v index 4e86049c1b9c..af7b2c8e90be 100644 --- a/theories/ssrmatching/ssrmatching.v +++ b/theories/ssrmatching/ssrmatching.v @@ -10,7 +10,7 @@ (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -Declare ML Module "coq-core.plugins.ssrmatching". +Declare ML Module "rocq-runtime.plugins.ssrmatching". Module SsrMatchingSyntax. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 612b4c9877cc..e3be92f9f87f 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -132,7 +132,7 @@ COQDEBUG ?= # Extra packages to be linked in (as in findlib -package) CAMLPKGS ?= -FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) +FINDLIBPKGS = -package rocq-runtime.plugins.ltac $(CAMLPKGS) # Option for making timing files TIMING?= diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 9af1e60bcd5c..65e783ed8c42 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -154,7 +154,7 @@ let generate_meta_file p = let meta : _ format = {| package "plugin" ( directory = "." - requires = "coq-core.plugins.ltac" + requires = "rocq-runtime.plugins.ltac" archive(byte) = "%s.cma" archive(native) = "%s.cmxa" plugin(byte) = "%s.cma" diff --git a/tools/coqdep/dune b/tools/coqdep/dune index add3becd0217..80227b6488b4 100644 --- a/tools/coqdep/dune +++ b/tools/coqdep/dune @@ -2,7 +2,7 @@ (executable (name coqdep) (public_name coqdep) - (package coq-core) + (package rocq-runtime) (modes exe byte) (modules coqdep) (libraries coqdeplib)) diff --git a/tools/coqdep/lib/dune b/tools/coqdep/lib/dune index 7a15877c908f..8c8fa56cff51 100644 --- a/tools/coqdep/lib/dune +++ b/tools/coqdep/lib/dune @@ -1,16 +1,16 @@ (library (name coqdeplib) - (public_name coq-core.coqdeplib) - (libraries coq-core.boot coq-core.lib findlib.internal)) + (public_name rocq-runtime.coqdeplib) + (libraries rocq-runtime.boot rocq-runtime.lib findlib.internal)) (ocamllex lexer) (rule (targets static_toplevel_libs.ml) - (deps %{workspace_root}/_build/install/%{context_name}/lib/coq-core/META) + (deps %{workspace_root}/_build/install/%{context_name}/lib/rocq-runtime/META) (action (with-stdout-to %{targets} - (run ocamlfind query -recursive -predicates native coq-core.toplevel + (run ocamlfind query -recursive -predicates native rocq-runtime.toplevel -prefix "let static_toplevel_libs = [\n" -format "\"%p\";" -suffix "\n]\n")))) diff --git a/tools/coqdep/lib/fl.ml b/tools/coqdep/lib/fl.ml index 065dcafe3bdc..afc76c5f2f47 100644 --- a/tools/coqdep/lib/fl.ml +++ b/tools/coqdep/lib/fl.ml @@ -94,7 +94,7 @@ let findlib_deep_resolve ~file ~package = module Internal = struct let get_worker_path () = let top = "coqworker" in - let dir = Findlib.package_directory "coq-core" in + let dir = Findlib.package_directory "rocq-runtime" in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in let file = Filename.concat dir (top^exe) in match Sys.getenv_opt "DUNE_SOURCEROOT" with diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/coqdoc.ml similarity index 100% rename from tools/coqdoc/main.ml rename to tools/coqdoc/coqdoc.ml diff --git a/tools/coqdoc/main.mli b/tools/coqdoc/coqdoc.mli similarity index 100% rename from tools/coqdoc/main.mli rename to tools/coqdoc/coqdoc.mli diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune index 54cff3fcd683..4d4ead038a55 100644 --- a/tools/coqdoc/dune +++ b/tools/coqdoc/dune @@ -1,6 +1,6 @@ (install (section lib) - (package coq-core) + (package rocq-runtime) (files (coqdoc.css as tools/coqdoc/coqdoc.css) (coqdoc.sty as tools/coqdoc/coqdoc.sty))) @@ -8,14 +8,14 @@ ; File needs to be here too. (install (section share_root) - (package coq-core) + (package rocq-runtime) (files (coqdoc.sty as texmf/tex/latex/misc/coqdoc.sty))) (executable - (name main) + (name coqdoc) (public_name coqdoc) - (package coq-core) - (libraries str coq-core.boot coq-core.config coq-core.clib)) + (package rocq-runtime) + (libraries str rocq-runtime.boot rocq-runtime.config rocq-runtime.clib)) (ocamllex cpretty) diff --git a/tools/coqworkmgr/dune b/tools/coqworkmgr/dune index d8c94161983e..eb9acda955e3 100644 --- a/tools/coqworkmgr/dune +++ b/tools/coqworkmgr/dune @@ -1,13 +1,17 @@ (library (name coqworkmgrlib) - (public_name coq-core.coqworkmgrapi) + (public_name rocq-runtime.coqworkmgrapi) (modules coqworkmgrApi) (wrapped false) (libraries str unix)) +(deprecated_library_name + (old_public_name coq-core.coqworkmgrapi) + (new_public_name rocq-runtime.coqworkmgrapi)) + (executable (name coqworkmgr) (public_name coqworkmgr) - (package coq-core) + (package rocq-runtime) (modules coqworkmgr) (libraries coqworkmgrlib)) diff --git a/tools/dune b/tools/dune index 790eb24ef204..3dcc23999710 100644 --- a/tools/dune +++ b/tools/dune @@ -1,12 +1,12 @@ (install (section lib) - (package coq-core) + (package rocq-runtime) (files (CoqMakefile.in as tools/CoqMakefile.in))) (install (section libexec) - (package coq-core) + (package rocq-runtime) (files (TimeFileMaker.py as tools/TimeFileMaker.py) (make-one-time-file.py as tools/make-one-time-file.py) @@ -16,15 +16,15 @@ (executable (name coq_makefile) (public_name coq_makefile) - (package coq-core) + (package rocq-runtime) (modules coq_makefile) - (libraries coq-core.boot coq-core.lib)) + (libraries rocq-runtime.boot rocq-runtime.lib)) ; Bare-bones mllib/mlpack parser (executable (name ocamllibdep) (public_name ocamllibdep) - (package coq-core) + (package rocq-runtime) (modules ocamllibdep) (libraries unix)) @@ -33,7 +33,7 @@ (executable (name coqwc) (public_name coqwc) - (package coq-core) + (package rocq-runtime) (modules coqwc) (libraries)) @@ -42,6 +42,6 @@ (executables (names coq_tex) (public_names coq-tex) - (package coq-core) + (package rocq-runtime) (modules coq_tex) (libraries str)) diff --git a/tools/dune_rule_gen/coq_rules.ml b/tools/dune_rule_gen/coq_rules.ml index f8bb2d5b5091..0be08c1de74a 100644 --- a/tools/dune_rule_gen/coq_rules.ml +++ b/tools/dune_rule_gen/coq_rules.ml @@ -24,7 +24,7 @@ module FlagUtil = struct (* Native flag *) let findlib_native_dir () = try - Findlib.package_directory ("coq-core.kernel") |> Path.make + Findlib.package_directory ("rocq-runtime.kernel") |> Path.make with Fl_package_base.No_such_package (p,_) -> raise (Invalid_argument ("failed to locate Coq kernel package in split build mode: " ^ p)) @@ -155,7 +155,7 @@ module Context = struct ] (* XXX: we could put the workers here, but they need a complete OCaml runtime so this is better *) - let build_async_deps = ["(package coq-core)"] + let build_async_deps = ["(package rocq-runtime)"] (* args are for coqdep *) let build_dep_info ~coqdep_args dir_info = diff --git a/tools/dune_rule_gen/coq_rules.mli b/tools/dune_rule_gen/coq_rules.mli index cf28eb4ec97a..4e66c210c924 100644 --- a/tools/dune_rule_gen/coq_rules.mli +++ b/tools/dune_rule_gen/coq_rules.mli @@ -48,7 +48,7 @@ module Context : sig -> rule:Coq_module.Rule_type.t (* quick, native, etc... *) -> async:bool -> dir_info:Coq_module.t Dir_info.t (* contents of the directory scan *) - -> split:bool (* whether we are building coq-core + rocq-core or only rocq-core *) + -> split:bool (* whether we are building rocq-runtime + rocq-core or only rocq-core *) -> t end diff --git a/tools/dune_rule_gen/dune b/tools/dune_rule_gen/dune index 8c8deded092b..c74562595fb6 100644 --- a/tools/dune_rule_gen/dune +++ b/tools/dune_rule_gen/dune @@ -2,7 +2,7 @@ (name coq_dune) (modules :standard \ gen_rules) (flags :standard -w +a-40-42) - (libraries coq-core.coqdeplib findlib)) + (libraries rocq-runtime.coqdeplib findlib)) (executable (name gen_rules) diff --git a/topbin/coqc_bin.ml b/topbin/coqc_bin.ml index f3094c6518a9..aaa1efb5dcbc 100644 --- a/topbin/coqc_bin.ml +++ b/topbin/coqc_bin.ml @@ -13,7 +13,7 @@ open Rocqshim let () = let args = List.tl (Array.to_list Sys.argv) in let {debug_shim}, args = Rocqshim.init args in - let prog = get_worker_path { package = "coq-core"; basename = "coqworker" } in + let prog = get_worker_path { package = "rocq-runtime"; basename = "coqworker" } in let () = if debug_shim then Printf.eprintf "Using %s\n%!" prog in let argv = Array.of_list (prog :: "--kind=compile" :: args) in exec_or_create_process prog argv diff --git a/topbin/dune b/topbin/dune index 3ddd1ee3212c..e6bec154543a 100644 --- a/topbin/dune +++ b/topbin/dune @@ -1,6 +1,6 @@ (library (name rocqshim) - (public_name coq-core.rocqshim) + (public_name rocq-runtime.rocqshim) (synopsis "Rocq support for finding and exec-ing subcommands") (wrapped false) ; no point repeating the Rocqshim name (modules rocqshim) @@ -8,44 +8,44 @@ (executable (public_name rocq) - (package coq-core) + (package rocq-runtime) (modules rocq) (modes exe byte) (libraries rocqshim)) (install (section bin) - (package coq-core) + (package rocq-runtime) (files (rocq.bc as rocq.byte))) (executable (name coqtop_bin) (public_name coqtop) - (package coq-core) + (package rocq-runtime) (modules coqtop_bin) - (libraries coq-core.toplevel)) + (libraries rocq-runtime.toplevel)) (executable (name coqtop_byte_bin) (public_name coqtop.byte) - (package coq-core) + (package rocq-runtime) (modules coqtop_byte_bin) - (libraries compiler-libs.toplevel coq-core.config.byte coq-core.toplevel coq-core.dev findlib.top) + (libraries compiler-libs.toplevel rocq-runtime.config.byte rocq-runtime.toplevel rocq-runtime.dev findlib.top) (modes byte)) (executable (name coqc_bin) (public_name coqc) - (package coq-core) + (package rocq-runtime) (modules coqc_bin) (libraries rocqshim)) (executable (name coqnative_bin) (public_name coqnative) - (package coq-core) + (package rocq-runtime) (modules coqnative_bin) - (libraries coq-core.kernel) + (libraries rocq-runtime.kernel) (modes exe byte) (link_flags -linkall)) @@ -54,13 +54,13 @@ (name coqworker_bin) (modules coqworker_bin) (modes exe byte) - (libraries coq-core.toplevel)) + (libraries rocq-runtime.toplevel)) ; Adding -ccopt -flto to links options could be interesting, however, ; it doesn't work on Windows (install (section libexec) - (package coq-core) + (package rocq-runtime) (files (coqworker_bin.exe as coqworker) (coqworker_bin.bc as coqworker.byte))) diff --git a/topbin/rocq.ml b/topbin/rocq.ml index 03f73e2b6b07..9435d0119a36 100644 --- a/topbin/rocq.ml +++ b/topbin/rocq.ml @@ -22,7 +22,7 @@ let () = match args with | "-v" :: _ | "--version" :: _ -> Boot.Usage.version () | ("c" | "compile") :: args -> - let prog = Rocqshim.get_worker_path { package = "coq-core"; basename = "coqworker" } in + let prog = Rocqshim.get_worker_path { package = "rocq-runtime"; basename = "coqworker" } in let () = if debug_shim then Printf.eprintf "Using %s\n%!" prog in let argv = Array.of_list (prog :: "--kind=compile" :: args) in Rocqshim.exec_or_create_process prog argv diff --git a/toplevel/dune b/toplevel/dune index 38b3f96d314c..1fe1b5fa6c31 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -1,15 +1,19 @@ (library (name toplevel) - (public_name coq-core.toplevel) + (public_name rocq-runtime.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) ; until ocaml/dune#4892 fixed ; (private_modules g_toplevel) - (libraries coq-core.stm + (libraries rocq-runtime.stm (select memtrace_init.ml from (memtrace -> memtrace_init.memtrace.ml) (!memtrace -> memtrace_init.default.ml)))) +(deprecated_library_name + (old_public_name coq-core.toplevel) + (new_public_name rocq-runtime.toplevel)) + ; Interp provides the `zarith` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v index 76951364c732..dc2adec6d2c8 100644 --- a/user-contrib/Ltac2/Array.v +++ b/user-contrib/Ltac2/Array.v @@ -34,14 +34,14 @@ Require Ltac2.Message. (* Question: what is returned in case of an out of range value? Answer: Ltac2 throws a panic *) -Ltac2 @external empty : 'a array := "coq-core.plugins.ltac2" "array_empty". -Ltac2 @external make : int -> 'a -> 'a array := "coq-core.plugins.ltac2" "array_make". -Ltac2 @external length : 'a array -> int := "coq-core.plugins.ltac2" "array_length". -Ltac2 @external get : 'a array -> int -> 'a := "coq-core.plugins.ltac2" "array_get". -Ltac2 @external set : 'a array -> int -> 'a -> unit := "coq-core.plugins.ltac2" "array_set". -Ltac2 @external lowlevel_blit : 'a array -> int -> 'a array -> int -> int -> unit := "coq-core.plugins.ltac2" "array_blit". -Ltac2 @external lowlevel_fill : 'a array -> int -> int -> 'a -> unit := "coq-core.plugins.ltac2" "array_fill". -Ltac2 @external concat : ('a array) list -> 'a array := "coq-core.plugins.ltac2" "array_concat". +Ltac2 @external empty : 'a array := "rocq-runtime.plugins.ltac2" "array_empty". +Ltac2 @external make : int -> 'a -> 'a array := "rocq-runtime.plugins.ltac2" "array_make". +Ltac2 @external length : 'a array -> int := "rocq-runtime.plugins.ltac2" "array_length". +Ltac2 @external get : 'a array -> int -> 'a := "rocq-runtime.plugins.ltac2" "array_get". +Ltac2 @external set : 'a array -> int -> 'a -> unit := "rocq-runtime.plugins.ltac2" "array_set". +Ltac2 @external lowlevel_blit : 'a array -> int -> 'a array -> int -> int -> unit := "rocq-runtime.plugins.ltac2" "array_blit". +Ltac2 @external lowlevel_fill : 'a array -> int -> int -> 'a -> unit := "rocq-runtime.plugins.ltac2" "array_fill". +Ltac2 @external concat : ('a array) list -> 'a array := "rocq-runtime.plugins.ltac2" "array_concat". (* Low level array operations *) diff --git a/user-contrib/Ltac2/Char.v b/user-contrib/Ltac2/Char.v index 3388a21c0591..437344554961 100644 --- a/user-contrib/Ltac2/Char.v +++ b/user-contrib/Ltac2/Char.v @@ -11,10 +11,10 @@ Require Import Ltac2.Init. Require Ltac2.Int. -Ltac2 @external of_int : int -> char := "coq-core.plugins.ltac2" "char_of_int". +Ltac2 @external of_int : int -> char := "rocq-runtime.plugins.ltac2" "char_of_int". (** Throws if the integer is not a valid char (in range [0-255]). *) -Ltac2 @external to_int : char -> int := "coq-core.plugins.ltac2" "char_to_int". +Ltac2 @external to_int : char -> int := "rocq-runtime.plugins.ltac2" "char_to_int". Ltac2 equal (x : char) (y : char) : bool := Int.equal (to_int x) (to_int y). Ltac2 compare (x : char) (y : char) : int := Int.compare (to_int x) (to_int y). diff --git a/user-contrib/Ltac2/Constant.v b/user-contrib/Ltac2/Constant.v index 0ba269d92460..b37db373c9ff 100644 --- a/user-contrib/Ltac2/Constant.v +++ b/user-contrib/Ltac2/Constant.v @@ -12,6 +12,6 @@ Require Import Ltac2.Init. Ltac2 Type t := constant. -Ltac2 @ external equal : constant -> constant -> bool := "coq-core.plugins.ltac2" "constant_equal". +Ltac2 @ external equal : constant -> constant -> bool := "rocq-runtime.plugins.ltac2" "constant_equal". (** Constants obtained through module aliases or Include are not considered equal by this function. *) diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 4718dac31ede..8149d4a77786 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -11,10 +11,10 @@ Require Import Ltac2.Init. Require Ltac2.Ind Ltac2.Array. -Ltac2 @ external type : constr -> constr := "coq-core.plugins.ltac2" "constr_type". +Ltac2 @ external type : constr -> constr := "rocq-runtime.plugins.ltac2" "constr_type". (** Return the type of a term *) -Ltac2 @ external equal : constr -> constr -> bool := "coq-core.plugins.ltac2" "constr_equal". +Ltac2 @ external equal : constr -> constr -> bool := "rocq-runtime.plugins.ltac2" "constr_equal". (** Strict syntactic equality: only up to α-conversion and evar expansion *) Module Binder. @@ -22,20 +22,20 @@ Module Binder. Ltac2 Type relevance_var. Ltac2 Type relevance := [ Relevant | Irrelevant | RelevanceVar (relevance_var) ]. -Ltac2 @ external make : ident option -> constr -> binder := "coq-core.plugins.ltac2" "constr_binder_make". +Ltac2 @ external make : ident option -> constr -> binder := "rocq-runtime.plugins.ltac2" "constr_binder_make". (** Create a binder given the name and the type of the bound variable. Fails if the type is not a type in the current goal. *) -Ltac2 @ external unsafe_make : ident option -> relevance -> constr -> binder := "coq-core.plugins.ltac2" "constr_binder_unsafe_make". +Ltac2 @ external unsafe_make : ident option -> relevance -> constr -> binder := "rocq-runtime.plugins.ltac2" "constr_binder_unsafe_make". (** Create a binder given the name and the type and relevance of the bound variable. *) -Ltac2 @ external name : binder -> ident option := "coq-core.plugins.ltac2" "constr_binder_name". +Ltac2 @ external name : binder -> ident option := "rocq-runtime.plugins.ltac2" "constr_binder_name". (** Retrieve the name of a binder. *) -Ltac2 @ external type : binder -> constr := "coq-core.plugins.ltac2" "constr_binder_type". +Ltac2 @ external type : binder -> constr := "rocq-runtime.plugins.ltac2" "constr_binder_type". (** Retrieve the type of a binder. *) -Ltac2 @ external relevance : binder -> relevance := "coq-core.plugins.ltac2" "constr_binder_relevance". +Ltac2 @ external relevance : binder -> relevance := "rocq-runtime.plugins.ltac2" "constr_binder_relevance". (** Retrieve the relevance of a binder. *) End Binder. @@ -75,7 +75,7 @@ Ltac2 Type kind := [ | Array (instance, constr array, constr, constr) ]. -Ltac2 @ external kind : constr -> kind := "coq-core.plugins.ltac2" "constr_kind". +Ltac2 @ external kind : constr -> kind := "rocq-runtime.plugins.ltac2" "constr_kind". Ltac2 rec kind_nocast c := match kind c with @@ -83,33 +83,33 @@ Ltac2 rec kind_nocast c := | k => k end. -Ltac2 @ external make : kind -> constr := "coq-core.plugins.ltac2" "constr_make". +Ltac2 @ external make : kind -> constr := "rocq-runtime.plugins.ltac2" "constr_make". -Ltac2 @ external check : constr -> constr result := "coq-core.plugins.ltac2" "constr_check". +Ltac2 @ external check : constr -> constr result := "rocq-runtime.plugins.ltac2" "constr_check". (** Checks that a constr generated by unsafe means is indeed safe in the current environment, and returns it, or the error otherwise. Panics if not focused. *) -Ltac2 @ external liftn : int -> int -> constr -> constr := "coq-core.plugins.ltac2" "constr_liftn". +Ltac2 @ external liftn : int -> int -> constr -> constr := "rocq-runtime.plugins.ltac2" "constr_liftn". (** [liftn n k c] lifts by [n] indices greater than or equal to [k] in [c] Note that with respect to substitution calculi's terminology, [n] is the _shift_ and [k] is the _lift_. *) -Ltac2 @ external substnl : constr list -> int -> constr -> constr := "coq-core.plugins.ltac2" "constr_substnl". +Ltac2 @ external substnl : constr list -> int -> constr -> constr := "rocq-runtime.plugins.ltac2" "constr_substnl". (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with [r₁;...;rₙ] in [c]. *) -Ltac2 @ external closenl : ident list -> int -> constr -> constr := "coq-core.plugins.ltac2" "constr_closenl". +Ltac2 @ external closenl : ident list -> int -> constr -> constr := "rocq-runtime.plugins.ltac2" "constr_closenl". (** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *) -Ltac2 @ external closedn : int -> constr -> bool := "coq-core.plugins.ltac2" "constr_closedn". +Ltac2 @ external closedn : int -> constr -> bool := "rocq-runtime.plugins.ltac2" "constr_closedn". (** [closedn n c] is true iff [c] is a closed term under [n] binders *) Ltac2 is_closed (c : constr) : bool := closedn 0 c. (** [is_closed c] is true iff [c] is a closed term (contains no [Rel]s) *) -Ltac2 @ external noccur_between : int -> int -> constr -> bool := "coq-core.plugins.ltac2" "constr_noccur_between". +Ltac2 @ external noccur_between : int -> int -> constr -> bool := "rocq-runtime.plugins.ltac2" "constr_noccur_between". (** [noccur_between n m c] returns true iff [Rel p] does not occur in term [c] for [n <= p < n+m] *) @@ -126,7 +126,7 @@ Use noccurn instead if you want [true] for variables which do not occur in the t and its negation if you want [false].")] Ltac2 occurn (n : int) (c : constr) : bool := noccur_between n 1 c. -Ltac2 @ external case : inductive -> case := "coq-core.plugins.ltac2" "constr_case". +Ltac2 @ external case : inductive -> case := "rocq-runtime.plugins.ltac2" "constr_case". (** Generate the case information for a given inductive type. *) Ltac2 constructor (ind : inductive) (i : int) : constructor := @@ -135,7 +135,7 @@ Ltac2 constructor (ind : inductive) (i : int) : constructor := at 0. Panics if there is no such constructor. *) Module Case. - Ltac2 @ external equal : case -> case -> bool := "coq-core.plugins.ltac2" "constr_case_equal". + Ltac2 @ external equal : case -> case -> bool := "rocq-runtime.plugins.ltac2" "constr_case_equal". (** Checks equality of the inductive components of the case info. When comparing the inductives, those obtained through module aliases or Include are not considered equal by this @@ -341,15 +341,15 @@ End Unsafe. Module Cast. - Ltac2 @ external default : cast := "coq-core.plugins.ltac2" "constr_cast_default". - Ltac2 @ external vm : cast := "coq-core.plugins.ltac2" "constr_cast_vm". - Ltac2 @ external native : cast := "coq-core.plugins.ltac2" "constr_cast_native". + Ltac2 @ external default : cast := "rocq-runtime.plugins.ltac2" "constr_cast_default". + Ltac2 @ external vm : cast := "rocq-runtime.plugins.ltac2" "constr_cast_vm". + Ltac2 @ external native : cast := "rocq-runtime.plugins.ltac2" "constr_cast_native". - Ltac2 @ external equal : cast -> cast -> bool := "coq-core.plugins.ltac2" "constr_cast_equal". + Ltac2 @ external equal : cast -> cast -> bool := "rocq-runtime.plugins.ltac2" "constr_cast_equal". End Cast. -Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "coq-core.plugins.ltac2" "constr_in_context". +Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "rocq-runtime.plugins.ltac2" "constr_in_context". (** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is the proof built by the tactic. *) @@ -358,26 +358,26 @@ Module Pretype. Module Flags. Ltac2 Type t. - Ltac2 @ external constr_flags : t := "coq-core.plugins.ltac2" "constr_flags". + Ltac2 @ external constr_flags : t := "rocq-runtime.plugins.ltac2" "constr_flags". (** The flags used by constr:(). *) Ltac2 @external set_use_coercions : bool -> t -> t - := "coq-core.plugins.ltac2" "pretype_flags_set_use_coercions". + := "rocq-runtime.plugins.ltac2" "pretype_flags_set_use_coercions". (** Use coercions during pretyping. [true] in [constr_flags]. *) Ltac2 @external set_use_typeclasses : bool -> t -> t - := "coq-core.plugins.ltac2" "pretype_flags_set_use_typeclasses". + := "rocq-runtime.plugins.ltac2" "pretype_flags_set_use_typeclasses". (** Run typeclass inference at the end of pretyping and when needed according to flag "Typeclass Resolution For Conversion". [true] in [constr_flags]. *) Ltac2 @external set_allow_evars : bool -> t -> t - := "coq-core.plugins.ltac2" "pretype_flags_set_allow_evars". + := "rocq-runtime.plugins.ltac2" "pretype_flags_set_allow_evars". (** Allow pretyping to produce new unresolved evars. [false] in [constr_flags]. *) Ltac2 @external set_nf_evars : bool -> t -> t - := "coq-core.plugins.ltac2" "pretype_flags_set_nf_evars". + := "rocq-runtime.plugins.ltac2" "pretype_flags_set_nf_evars". (** Evar-normalize the result of pretyping. This should not impact anything other than performance. [true] in [constr_flags]. *) @@ -399,16 +399,16 @@ Module Pretype. Ltac2 Type expected_type. Ltac2 @ external expected_istype : expected_type - := "coq-core.plugins.ltac2" "expected_istype". + := "rocq-runtime.plugins.ltac2" "expected_istype". Ltac2 @ external expected_oftype : constr -> expected_type - := "coq-core.plugins.ltac2" "expected_oftype". + := "rocq-runtime.plugins.ltac2" "expected_oftype". Ltac2 @ external expected_without_type_constraint : expected_type - := "coq-core.plugins.ltac2" "expected_without_type_constraint". + := "rocq-runtime.plugins.ltac2" "expected_without_type_constraint". Ltac2 @ external pretype : Flags.t -> expected_type -> preterm -> constr - := "coq-core.plugins.ltac2" "constr_pretype". + := "rocq-runtime.plugins.ltac2" "constr_pretype". (** Pretype the provided preterm. Assumes the goal to be focussed. *) End Pretype. @@ -423,7 +423,7 @@ Ltac2 is_evar(c: constr) := | _ => false end. -Ltac2 @ external has_evar : constr -> bool := "coq-core.plugins.ltac2" "constr_has_evar". +Ltac2 @ external has_evar : constr -> bool := "rocq-runtime.plugins.ltac2" "constr_has_evar". Ltac2 is_var(c: constr) := match Unsafe.kind c with diff --git a/user-contrib/Ltac2/Constructor.v b/user-contrib/Ltac2/Constructor.v index dcc0d209654d..98a7c3fabba1 100644 --- a/user-contrib/Ltac2/Constructor.v +++ b/user-contrib/Ltac2/Constructor.v @@ -12,13 +12,13 @@ Require Import Ltac2.Init. Ltac2 Type t := constructor. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "constructor_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "constructor_equal". (** Constructors obtained through module aliases or Include are not considered equal by this function. *) -Ltac2 @ external inductive : t -> inductive := "coq-core.plugins.ltac2" "constructor_inductive". +Ltac2 @ external inductive : t -> inductive := "rocq-runtime.plugins.ltac2" "constructor_inductive". (** Returns the inductive to which the given constructor belongs. *) -Ltac2 @ external index : t -> int := "coq-core.plugins.ltac2" "constructor_index". +Ltac2 @ external index : t -> int := "rocq-runtime.plugins.ltac2" "constructor_index". (** Returns the index of the given constructor (such that [c] is [Ind.get_constructor (Ind.data (inductive c)) (index c)]). *) diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v index b999a2c8ebf8..86f8b8a97bfc 100644 --- a/user-contrib/Ltac2/Control.v +++ b/user-contrib/Ltac2/Control.v @@ -13,63 +13,63 @@ Require Ltac2.Message. (** Panic *) -Ltac2 @ external throw : exn -> 'a := "coq-core.plugins.ltac2" "throw". +Ltac2 @ external throw : exn -> 'a := "rocq-runtime.plugins.ltac2" "throw". (** Fatal exception throwing. This does not induce backtracking. *) (** Generic backtracking control *) -Ltac2 @ external zero : exn -> 'a := "coq-core.plugins.ltac2" "zero". -Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "coq-core.plugins.ltac2" "plus". -Ltac2 @ external once : (unit -> 'a) -> 'a := "coq-core.plugins.ltac2" "once". -Ltac2 @ external case : (unit -> 'a) -> ('a * (exn -> 'a)) result := "coq-core.plugins.ltac2" "case". +Ltac2 @ external zero : exn -> 'a := "rocq-runtime.plugins.ltac2" "zero". +Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "plus". +Ltac2 @ external once : (unit -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "once". +Ltac2 @ external case : (unit -> 'a) -> ('a * (exn -> 'a)) result := "rocq-runtime.plugins.ltac2" "case". Ltac2 once_plus (run : unit -> 'a) (handle : exn -> 'a) : 'a := once (fun () => plus run handle). (** Proof state manipulation *) -Ltac2 @ external numgoals : unit -> int := "coq-core.plugins.ltac2" "numgoals". +Ltac2 @ external numgoals : unit -> int := "rocq-runtime.plugins.ltac2" "numgoals". (** Return the number of goals currently focused. *) -Ltac2 @ external dispatch : (unit -> unit) list -> unit := "coq-core.plugins.ltac2" "dispatch". -Ltac2 @ external extend : (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit := "coq-core.plugins.ltac2" "extend". -Ltac2 @ external enter : (unit -> unit) -> unit := "coq-core.plugins.ltac2" "enter". +Ltac2 @ external dispatch : (unit -> unit) list -> unit := "rocq-runtime.plugins.ltac2" "dispatch". +Ltac2 @ external extend : (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit := "rocq-runtime.plugins.ltac2" "extend". +Ltac2 @ external enter : (unit -> unit) -> unit := "rocq-runtime.plugins.ltac2" "enter". -Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "coq-core.plugins.ltac2" "focus". -Ltac2 @ external shelve : unit -> unit := "coq-core.plugins.ltac2" "shelve". -Ltac2 @ external shelve_unifiable : unit -> unit := "coq-core.plugins.ltac2" "shelve_unifiable". +Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "focus". +Ltac2 @ external shelve : unit -> unit := "rocq-runtime.plugins.ltac2" "shelve". +Ltac2 @ external shelve_unifiable : unit -> unit := "rocq-runtime.plugins.ltac2" "shelve_unifiable". -Ltac2 @ external new_goal : evar -> unit := "coq-core.plugins.ltac2" "new_goal". +Ltac2 @ external new_goal : evar -> unit := "rocq-runtime.plugins.ltac2" "new_goal". (** Adds the given evar to the list of goals as the last one. If it is already defined in the current state, don't do anything. Panics if the evar is not in the current state. *) -Ltac2 @ external unshelve : (unit -> 'a) -> 'a := "coq-core.plugins.ltac2" "unshelve". +Ltac2 @ external unshelve : (unit -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "unshelve". (** Runs the closure, then unshelves existential variables added to the shelf by its execution, prepending them to the current goal. Returns the value produced by the closure. *) -Ltac2 @ external progress : (unit -> 'a) -> 'a := "coq-core.plugins.ltac2" "progress". +Ltac2 @ external progress : (unit -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "progress". (** Goal inspection *) -Ltac2 @ external goal : unit -> constr := "coq-core.plugins.ltac2" "goal". +Ltac2 @ external goal : unit -> constr := "rocq-runtime.plugins.ltac2" "goal". (** Panics if there is not exactly one goal under focus. Otherwise returns the conclusion of this goal. *) -Ltac2 @ external hyp : ident -> constr := "coq-core.plugins.ltac2" "hyp". +Ltac2 @ external hyp : ident -> constr := "rocq-runtime.plugins.ltac2" "hyp". (** Panics if there is more than one goal under focus. If there is no goal under focus, looks for the section variable with the given name. If there is one, looks for the hypothesis with the given name. *) -Ltac2 @ external hyp_value : ident -> constr option := "coq-core.plugins.ltac2" "hyp_value". +Ltac2 @ external hyp_value : ident -> constr option := "rocq-runtime.plugins.ltac2" "hyp_value". (** Panics if there is more than one goal under focus. If there is no goal under focus, looks for the section variable with the given name and return its value ("v" in "H := v") if there is one. If there is one, looks for the hypothesis with the given name and return its value if there is one. *) -Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "coq-core.plugins.ltac2" "hyps". +Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "rocq-runtime.plugins.ltac2" "hyps". (** Panics if there is more than one goal under focus. If there is no goal under focus, returns the list of section variables. If there is one, returns the list of hypotheses. In both cases, the @@ -77,24 +77,24 @@ Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "coq-co (** Refinement *) -Ltac2 @ external refine : (unit -> constr) -> unit := "coq-core.plugins.ltac2" "refine". +Ltac2 @ external refine : (unit -> constr) -> unit := "rocq-runtime.plugins.ltac2" "refine". (** Evars *) -Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "coq-core.plugins.ltac2" "with_holes". +Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "rocq-runtime.plugins.ltac2" "with_holes". (** [with_holes x f] evaluates [x], then apply [f] to the result, and fails if all evars generated by the call to [x] have not been solved when [f] returns. *) (** Misc *) -Ltac2 @ external time : string option -> (unit -> 'a) -> 'a := "coq-core.plugins.ltac2" "time". +Ltac2 @ external time : string option -> (unit -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "time". (** Displays the time taken by a tactic to evaluate. *) -Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "coq-core.plugins.ltac2" "abstract". +Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "rocq-runtime.plugins.ltac2" "abstract". (** Abstract a subgoal. *) -Ltac2 @ external check_interrupt : unit -> unit := "coq-core.plugins.ltac2" "check_interrupt". +Ltac2 @ external check_interrupt : unit -> unit := "rocq-runtime.plugins.ltac2" "check_interrupt". (** For internal use. *) (** Assertions throwing exceptions and short form throws *) @@ -133,12 +133,12 @@ Ltac2 backtrack_tactic_failure (msg : string) := (** [throw_bt info e] is similar to [throw e], but raises [e] with the backtrace represented by [info]. *) Ltac2 @ external throw_bt : exn -> exninfo -> 'a := - "coq-core.plugins.ltac2" "throw_bt". + "rocq-runtime.plugins.ltac2" "throw_bt". (** [zero_bt info e] is similar to [zero e], but raises [e] with the backtrace represented by [info]. *) Ltac2 @ external zero_bt : exn -> exninfo -> 'a := - "coq-core.plugins.ltac2" "zero_bt". + "rocq-runtime.plugins.ltac2" "zero_bt". (** [plus_bt run handle] is similar to [plus run handle] (up to the type missmatch for [handle]), but it calls [handle] with an extra argument @@ -146,7 +146,7 @@ Ltac2 @ external zero_bt : exn -> exninfo -> 'a := function can thus decide to re-attach that backtrace when using the [throw_bt] or [zero_bt] functions. *) Ltac2 @ external plus_bt : (unit -> 'a) -> (exn -> exninfo -> 'a) -> 'a := - "coq-core.plugins.ltac2" "plus_bt". + "rocq-runtime.plugins.ltac2" "plus_bt". (** [once_plus_bt run handle] is a non-backtracking variant of [once_plus] that has backtrace support similar to that of [plus_bt]. *) @@ -154,7 +154,7 @@ Ltac2 once_plus_bt (run : unit -> 'a) (handle : exn -> exninfo -> 'a) : 'a := once (fun _ => plus_bt run handle). Ltac2 @ external clear_err_info : err -> err := - "coq-core.plugins.ltac2" "clear_err_info". + "rocq-runtime.plugins.ltac2" "clear_err_info". Ltac2 clear_exn_info (e : exn) : exn := match e with @@ -166,8 +166,8 @@ Ltac2 clear_exn_info (e : exn) : exn := (** [timeout t thunk] calls [thunk ()] with a timeout of [t] seconds. *) Ltac2 @ external timeout : int -> (unit -> 'a) -> 'a := - "coq-core.plugins.ltac2" "timeout". + "rocq-runtime.plugins.ltac2" "timeout". (** [timeoutf t thunk] calls [thunk ()] with a timeout of [t] seconds. *) Ltac2 @ external timeoutf : float -> (unit -> 'a) -> 'a := - "coq-core.plugins.ltac2" "timeoutf". + "rocq-runtime.plugins.ltac2" "timeoutf". diff --git a/user-contrib/Ltac2/Env.v b/user-contrib/Ltac2/Env.v index f6973bc56eaa..d63b8242049e 100644 --- a/user-contrib/Ltac2/Env.v +++ b/user-contrib/Ltac2/Env.v @@ -10,19 +10,19 @@ From Ltac2 Require Import Init Std. -Ltac2 @ external get : ident list -> Std.reference option := "coq-core.plugins.ltac2" "env_get". +Ltac2 @ external get : ident list -> Std.reference option := "rocq-runtime.plugins.ltac2" "env_get". (** Returns the global reference corresponding to the absolute name given as argument if it exists. *) -Ltac2 @ external expand : ident list -> Std.reference list := "coq-core.plugins.ltac2" "env_expand". +Ltac2 @ external expand : ident list -> Std.reference list := "rocq-runtime.plugins.ltac2" "env_expand". (** Returns the list of all global references whose absolute name contains the argument list as a suffix. *) -Ltac2 @ external path : Std.reference -> ident list := "coq-core.plugins.ltac2" "env_path". +Ltac2 @ external path : Std.reference -> ident list := "rocq-runtime.plugins.ltac2" "env_path". (** Returns the absolute name of the given reference. Panics if the reference does not exist. *) -Ltac2 @ external instantiate : Std.reference -> constr := "coq-core.plugins.ltac2" "env_instantiate". +Ltac2 @ external instantiate : Std.reference -> constr := "rocq-runtime.plugins.ltac2" "env_instantiate". (** Returns a fresh instance of the corresponding reference, in particular generating fresh universe variables and constraints when this reference is universe-polymorphic. *) diff --git a/user-contrib/Ltac2/Evar.v b/user-contrib/Ltac2/Evar.v index 7708ce457824..ec3765c1396f 100644 --- a/user-contrib/Ltac2/Evar.v +++ b/user-contrib/Ltac2/Evar.v @@ -12,4 +12,4 @@ Require Import Ltac2.Init. Ltac2 Type t := evar. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "evar_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "evar_equal". diff --git a/user-contrib/Ltac2/FMap.v b/user-contrib/Ltac2/FMap.v index fd4fc59acf3c..50ef0bc4601c 100644 --- a/user-contrib/Ltac2/FMap.v +++ b/user-contrib/Ltac2/FMap.v @@ -15,24 +15,24 @@ Import FSet.Tags. Ltac2 Type ('k, 'v) t. -Ltac2 @ external empty : 'k tag -> ('k, 'v) t := "coq-core.plugins.ltac2" "fmap_empty". +Ltac2 @ external empty : 'k tag -> ('k, 'v) t := "rocq-runtime.plugins.ltac2" "fmap_empty". -Ltac2 @ external is_empty : ('k, 'v) t -> bool := "coq-core.plugins.ltac2" "fmap_is_empty". +Ltac2 @ external is_empty : ('k, 'v) t -> bool := "rocq-runtime.plugins.ltac2" "fmap_is_empty". -Ltac2 @ external mem : 'k -> ('k, 'v) t -> bool := "coq-core.plugins.ltac2" "fmap_mem". +Ltac2 @ external mem : 'k -> ('k, 'v) t -> bool := "rocq-runtime.plugins.ltac2" "fmap_mem". -Ltac2 @ external add : 'k -> 'v -> ('k, 'v) t -> ('k, 'v) t := "coq-core.plugins.ltac2" "fmap_add". +Ltac2 @ external add : 'k -> 'v -> ('k, 'v) t -> ('k, 'v) t := "rocq-runtime.plugins.ltac2" "fmap_add". -Ltac2 @ external remove : 'k -> ('k, 'v) t -> ('k, 'v) t := "coq-core.plugins.ltac2" "fmap_remove". +Ltac2 @ external remove : 'k -> ('k, 'v) t -> ('k, 'v) t := "rocq-runtime.plugins.ltac2" "fmap_remove". -Ltac2 @ external find_opt : 'k -> ('k, 'v) t -> 'v option := "coq-core.plugins.ltac2" "fmap_find_opt". +Ltac2 @ external find_opt : 'k -> ('k, 'v) t -> 'v option := "rocq-runtime.plugins.ltac2" "fmap_find_opt". -Ltac2 @ external mapi : ('k -> 'v -> 'r) -> ('k, 'v) t -> ('k, 'r) t := "coq-core.plugins.ltac2" "fmap_mapi". +Ltac2 @ external mapi : ('k -> 'v -> 'r) -> ('k, 'v) t -> ('k, 'r) t := "rocq-runtime.plugins.ltac2" "fmap_mapi". -Ltac2 @ external fold : ('k -> 'v -> 'acc -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc := "coq-core.plugins.ltac2" "fmap_fold". +Ltac2 @ external fold : ('k -> 'v -> 'acc -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc := "rocq-runtime.plugins.ltac2" "fmap_fold". -Ltac2 @ external cardinal : ('k, 'v) t -> int := "coq-core.plugins.ltac2" "fmap_cardinal". +Ltac2 @ external cardinal : ('k, 'v) t -> int := "rocq-runtime.plugins.ltac2" "fmap_cardinal". -Ltac2 @ external bindings : ('k, 'v) t -> ('k * 'v) list := "coq-core.plugins.ltac2" "fmap_bindings". +Ltac2 @ external bindings : ('k, 'v) t -> ('k * 'v) list := "rocq-runtime.plugins.ltac2" "fmap_bindings". -Ltac2 @ external domain : ('k, 'v) t -> 'k FSet.t := "coq-core.plugins.ltac2" "fmap_domain". +Ltac2 @ external domain : ('k, 'v) t -> 'k FSet.t := "rocq-runtime.plugins.ltac2" "fmap_domain". diff --git a/user-contrib/Ltac2/FSet.v b/user-contrib/Ltac2/FSet.v index f0a97af4d14b..ed9a674abfe5 100644 --- a/user-contrib/Ltac2/FSet.v +++ b/user-contrib/Ltac2/FSet.v @@ -13,38 +13,38 @@ From Ltac2 Require Import Init. Module Import Tags. Ltac2 Type 'a tag. - Ltac2 @ external ident_tag : ident tag := "coq-core.plugins.ltac2" "fmap_ident_tag". - Ltac2 @ external int_tag : int tag := "coq-core.plugins.ltac2" "fmap_int_tag". - Ltac2 @ external inductive_tag : inductive tag := "coq-core.plugins.ltac2" "fmap_inductive_tag". - Ltac2 @ external constructor_tag : constructor tag := "coq-core.plugins.ltac2" "fmap_constructor_tag". - Ltac2 @ external constant_tag : constant tag := "coq-core.plugins.ltac2" "fmap_constant_tag". + Ltac2 @ external ident_tag : ident tag := "rocq-runtime.plugins.ltac2" "fmap_ident_tag". + Ltac2 @ external int_tag : int tag := "rocq-runtime.plugins.ltac2" "fmap_int_tag". + Ltac2 @ external inductive_tag : inductive tag := "rocq-runtime.plugins.ltac2" "fmap_inductive_tag". + Ltac2 @ external constructor_tag : constructor tag := "rocq-runtime.plugins.ltac2" "fmap_constructor_tag". + Ltac2 @ external constant_tag : constant tag := "rocq-runtime.plugins.ltac2" "fmap_constant_tag". (* NB: strings are copied when keys are added and read to prevent mutation *) - Ltac2 @ external string_tag : string tag := "coq-core.plugins.ltac2" "fmap_string_tag". + Ltac2 @ external string_tag : string tag := "rocq-runtime.plugins.ltac2" "fmap_string_tag". End Tags. Ltac2 Type 'a t. -Ltac2 @ external empty : 'a tag -> 'a t := "coq-core.plugins.ltac2" "fset_empty". +Ltac2 @ external empty : 'a tag -> 'a t := "rocq-runtime.plugins.ltac2" "fset_empty". -Ltac2 @ external is_empty : 'a t -> bool := "coq-core.plugins.ltac2" "fset_is_empty". +Ltac2 @ external is_empty : 'a t -> bool := "rocq-runtime.plugins.ltac2" "fset_is_empty". -Ltac2 @ external mem : 'a -> 'a t -> bool := "coq-core.plugins.ltac2" "fset_mem". +Ltac2 @ external mem : 'a -> 'a t -> bool := "rocq-runtime.plugins.ltac2" "fset_mem". -Ltac2 @ external add : 'a -> 'a t -> 'a t := "coq-core.plugins.ltac2" "fset_add". +Ltac2 @ external add : 'a -> 'a t -> 'a t := "rocq-runtime.plugins.ltac2" "fset_add". -Ltac2 @ external remove : 'a -> 'a t -> 'a t := "coq-core.plugins.ltac2" "fset_remove". +Ltac2 @ external remove : 'a -> 'a t -> 'a t := "rocq-runtime.plugins.ltac2" "fset_remove". -Ltac2 @ external union : 'a t -> 'a t -> 'a t := "coq-core.plugins.ltac2" "fset_union". +Ltac2 @ external union : 'a t -> 'a t -> 'a t := "rocq-runtime.plugins.ltac2" "fset_union". -Ltac2 @ external inter : 'a t -> 'a t -> 'a t := "coq-core.plugins.ltac2" "fset_inter". +Ltac2 @ external inter : 'a t -> 'a t -> 'a t := "rocq-runtime.plugins.ltac2" "fset_inter". -Ltac2 @ external diff : 'a t -> 'a t -> 'a t := "coq-core.plugins.ltac2" "fset_diff". +Ltac2 @ external diff : 'a t -> 'a t -> 'a t := "rocq-runtime.plugins.ltac2" "fset_diff". -Ltac2 @ external equal : 'a t -> 'a t -> bool := "coq-core.plugins.ltac2" "fset_equal". +Ltac2 @ external equal : 'a t -> 'a t -> bool := "rocq-runtime.plugins.ltac2" "fset_equal". -Ltac2 @ external subset : 'a t -> 'a t -> bool := "coq-core.plugins.ltac2" "fset_subset". +Ltac2 @ external subset : 'a t -> 'a t -> bool := "rocq-runtime.plugins.ltac2" "fset_subset". -Ltac2 @ external cardinal : 'a t -> int := "coq-core.plugins.ltac2" "fset_cardinal". +Ltac2 @ external cardinal : 'a t -> int := "rocq-runtime.plugins.ltac2" "fset_cardinal". -Ltac2 @ external elements : 'a t -> 'a list := "coq-core.plugins.ltac2" "fset_elements". +Ltac2 @ external elements : 'a t -> 'a list := "rocq-runtime.plugins.ltac2" "fset_elements". diff --git a/user-contrib/Ltac2/Float.v b/user-contrib/Ltac2/Float.v index c2438cc9aeae..8aaa1680f5a5 100644 --- a/user-contrib/Ltac2/Float.v +++ b/user-contrib/Ltac2/Float.v @@ -12,4 +12,4 @@ Require Import Ltac2.Init. Ltac2 Type t := float. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "float_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "float_equal". diff --git a/user-contrib/Ltac2/Fresh.v b/user-contrib/Ltac2/Fresh.v index 94026fcbdc26..06c38f8dce7d 100644 --- a/user-contrib/Ltac2/Fresh.v +++ b/user-contrib/Ltac2/Fresh.v @@ -17,17 +17,17 @@ Module Free. Ltac2 Type t. (** Type of sets of free variables *) -Ltac2 @ external union : t -> t -> t := "coq-core.plugins.ltac2" "fresh_free_union". +Ltac2 @ external union : t -> t -> t := "rocq-runtime.plugins.ltac2" "fresh_free_union". -Ltac2 @ external of_ids : ident list -> t := "coq-core.plugins.ltac2" "fresh_free_of_ids". +Ltac2 @ external of_ids : ident list -> t := "rocq-runtime.plugins.ltac2" "fresh_free_of_ids". -Ltac2 @ external of_constr : constr -> t := "coq-core.plugins.ltac2" "fresh_free_of_constr". +Ltac2 @ external of_constr : constr -> t := "rocq-runtime.plugins.ltac2" "fresh_free_of_constr". Ltac2 of_goal () := of_ids (List.map (fun (id, _, _) => id) (Control.hyps ())). End Free. -Ltac2 @ external fresh : Free.t -> ident -> ident := "coq-core.plugins.ltac2" "fresh_fresh". +Ltac2 @ external fresh : Free.t -> ident -> ident := "rocq-runtime.plugins.ltac2" "fresh_fresh". (** Generate a fresh identifier with the given base name which is not a member of the provided set of free variables. *) diff --git a/user-contrib/Ltac2/Ident.v b/user-contrib/Ltac2/Ident.v index 38d93ee36035..bab7f22b76c1 100644 --- a/user-contrib/Ltac2/Ident.v +++ b/user-contrib/Ltac2/Ident.v @@ -12,8 +12,8 @@ Require Import Ltac2.Init. Ltac2 Type t := ident. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "ident_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "ident_equal". -Ltac2 @ external of_string : string -> t option := "coq-core.plugins.ltac2" "ident_of_string". +Ltac2 @ external of_string : string -> t option := "rocq-runtime.plugins.ltac2" "ident_of_string". -Ltac2 @ external to_string : t -> string := "coq-core.plugins.ltac2" "ident_to_string". +Ltac2 @ external to_string : t -> string := "rocq-runtime.plugins.ltac2" "ident_to_string". diff --git a/user-contrib/Ltac2/Ind.v b/user-contrib/Ltac2/Ind.v index 388b64edad28..ae05d6de650e 100644 --- a/user-contrib/Ltac2/Ind.v +++ b/user-contrib/Ltac2/Ind.v @@ -12,39 +12,39 @@ From Ltac2 Require Import Init. Ltac2 Type t := inductive. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "ind_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "ind_equal". (** Equality test. *) Ltac2 Type data. (** Type of data representing inductive blocks. *) -Ltac2 @ external data : t -> data := "coq-core.plugins.ltac2" "ind_data". +Ltac2 @ external data : t -> data := "rocq-runtime.plugins.ltac2" "ind_data". (** Get the mutual blocks corresponding to an inductive type in the current environment. Panics if there is no such inductive. *) -Ltac2 @ external repr : data -> t := "coq-core.plugins.ltac2" "ind_repr". +Ltac2 @ external repr : data -> t := "rocq-runtime.plugins.ltac2" "ind_repr". (** Returns the inductive corresponding to the block. Inverse of [data]. *) -Ltac2 @ external index : t -> int := "coq-core.plugins.ltac2" "ind_index". +Ltac2 @ external index : t -> int := "rocq-runtime.plugins.ltac2" "ind_index". (** Returns the index of the inductive type inside its mutual block. Guaranteed to range between [0] and [nblocks data - 1] where [data] was retrieved using the above function. *) -Ltac2 @ external nblocks : data -> int := "coq-core.plugins.ltac2" "ind_nblocks". +Ltac2 @ external nblocks : data -> int := "rocq-runtime.plugins.ltac2" "ind_nblocks". (** Returns the number of inductive types appearing in a mutual block. *) -Ltac2 @ external nconstructors : data -> int := "coq-core.plugins.ltac2" "ind_nconstructors". +Ltac2 @ external nconstructors : data -> int := "rocq-runtime.plugins.ltac2" "ind_nconstructors". (** Returns the number of constructors appearing in the current block. *) -Ltac2 @ external get_block : data -> int -> data := "coq-core.plugins.ltac2" "ind_get_block". +Ltac2 @ external get_block : data -> int -> data := "rocq-runtime.plugins.ltac2" "ind_get_block". (** Returns the block corresponding to the nth inductive type. Index must range between [0] and [nblocks data - 1], otherwise the function panics. *) -Ltac2 @ external get_constructor : data -> int -> constructor := "coq-core.plugins.ltac2" "ind_get_constructor". +Ltac2 @ external get_constructor : data -> int -> constructor := "rocq-runtime.plugins.ltac2" "ind_get_constructor". (** Returns the nth constructor of the inductive type. Index must range between [0] and [nconstructors data - 1], otherwise the function panics. *) Ltac2 @ external get_projections : data -> projection array option - := "coq-core.plugins.ltac2" "ind_get_projections". + := "rocq-runtime.plugins.ltac2" "ind_get_projections". (** Returns the list of projections for a primitive record, or [None] if the inductive is not a primitive record. *) diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index d96899fd0f53..2b8ddc9adf28 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -9,8 +9,8 @@ (************************************************************************) (* EJGA: Seems that Coq's findlib loader is not loading this correctly? *) -Declare ML Module "coq-core.plugins.ltac2". -Declare ML Module "coq-core.plugins.ltac2_ltac1". +Declare ML Module "rocq-runtime.plugins.ltac2". +Declare ML Module "rocq-runtime.plugins.ltac2_ltac1". #[export] Set Default Proof Mode "Ltac2". diff --git a/user-contrib/Ltac2/Int.v b/user-contrib/Ltac2/Int.v index 8b2ce2806f9c..e59b2aa74945 100644 --- a/user-contrib/Ltac2/Int.v +++ b/user-contrib/Ltac2/Int.v @@ -12,26 +12,26 @@ Require Import Ltac2.Init. Ltac2 Type t := int. -Ltac2 @ external equal : int -> int -> bool := "coq-core.plugins.ltac2" "int_equal". -Ltac2 @ external compare : int -> int -> int := "coq-core.plugins.ltac2" "int_compare". -Ltac2 @ external add : int -> int -> int := "coq-core.plugins.ltac2" "int_add". -Ltac2 @ external sub : int -> int -> int := "coq-core.plugins.ltac2" "int_sub". -Ltac2 @ external mul : int -> int -> int := "coq-core.plugins.ltac2" "int_mul". +Ltac2 @ external equal : int -> int -> bool := "rocq-runtime.plugins.ltac2" "int_equal". +Ltac2 @ external compare : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_compare". +Ltac2 @ external add : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_add". +Ltac2 @ external sub : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_sub". +Ltac2 @ external mul : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_mul". (* Note: unlike Coq Z division, Ltac2 matches OCaml division and rounds towards 0, so 1/-2 = 0 *) -Ltac2 @ external div : int -> int -> int := "coq-core.plugins.ltac2" "int_div". +Ltac2 @ external div : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_div". -Ltac2 @ external mod : int -> int -> int := "coq-core.plugins.ltac2" "int_mod". -Ltac2 @ external neg : int -> int := "coq-core.plugins.ltac2" "int_neg". -Ltac2 @ external abs : int -> int := "coq-core.plugins.ltac2" "int_abs". +Ltac2 @ external mod : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_mod". +Ltac2 @ external neg : int -> int := "rocq-runtime.plugins.ltac2" "int_neg". +Ltac2 @ external abs : int -> int := "rocq-runtime.plugins.ltac2" "int_abs". -Ltac2 @ external asr : int -> int -> int := "coq-core.plugins.ltac2" "int_asr". -Ltac2 @ external lsl : int -> int -> int := "coq-core.plugins.ltac2" "int_lsl". -Ltac2 @ external lsr : int -> int -> int := "coq-core.plugins.ltac2" "int_lsr". -Ltac2 @ external land : int -> int -> int := "coq-core.plugins.ltac2" "int_land". -Ltac2 @ external lor : int -> int -> int := "coq-core.plugins.ltac2" "int_lor". -Ltac2 @ external lxor : int -> int -> int := "coq-core.plugins.ltac2" "int_lxor". -Ltac2 @ external lnot : int -> int := "coq-core.plugins.ltac2" "int_lnot". +Ltac2 @ external asr : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_asr". +Ltac2 @ external lsl : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_lsl". +Ltac2 @ external lsr : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_lsr". +Ltac2 @ external land : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_land". +Ltac2 @ external lor : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_lor". +Ltac2 @ external lxor : int -> int -> int := "rocq-runtime.plugins.ltac2" "int_lxor". +Ltac2 @ external lnot : int -> int := "rocq-runtime.plugins.ltac2" "int_lnot". Ltac2 lt (x : int) (y : int) := equal (compare x y) -1. Ltac2 gt (x : int) (y : int) := equal (compare x y) 1. diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index f2331e7a4220..52752bc1954e 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/user-contrib/Ltac2/Ltac1.v @@ -18,50 +18,50 @@ Require Import Ltac2.Init Ltac2.Std Ltac2.Control. Ltac2 Type t. (** Dynamically-typed Ltac1 values. *) -Ltac2 @ external ref : ident list -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_ref". +Ltac2 @ external ref : ident list -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_ref". (** Returns the Ltac1 definition with the given absolute name. *) -Ltac2 @ external run : t -> unit := "coq-core.plugins.ltac2_ltac1" "ltac1_run". +Ltac2 @ external run : t -> unit := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_run". (** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning anything. *) -Ltac2 @ external lambda : (t -> t) -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_lambda". +Ltac2 @ external lambda : (t -> t) -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_lambda". (** Embed an Ltac2 function into Ltac1 values. Contrarily to the ltac1:(...) quotation, this function allows both to capture an Ltac2 context inside the closure and to return an Ltac1 value. Returning values in Ltac1 is a intrepid endeavour prone to weird runtime semantics. *) -Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "coq-core.plugins.ltac2_ltac1" "ltac1_apply". +Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_apply". (** Applies an Ltac1 value to a list of arguments, and provides the result in CPS style. It does **not** run the returned value. *) (** Conversion functions *) -Ltac2 @ external of_int : int -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_int". +Ltac2 @ external of_int : int -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_of_int". (** Converts an Ltac2 int into an Ltac1 value. *) -Ltac2 @ external to_int : t -> int option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_int". +Ltac2 @ external to_int : t -> int option := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_to_int". (** Converts an Ltac1 int into an Ltac2 value. *) -Ltac2 @ external of_constr : constr -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_constr". +Ltac2 @ external of_constr : constr -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_of_constr". (** Converts an Ltac2 constr into an Ltac1 value. *) -Ltac2 @ external to_constr : t -> constr option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_constr". +Ltac2 @ external to_constr : t -> constr option := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_to_constr". (** Converts an Ltac1 constr (which includes terms created via open_constr) into an Ltac2 value. *) (** [preterm] is called [uconstr] in Ltac1. *) -Ltac2 @ external of_preterm : preterm -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_preterm". -Ltac2 @ external to_preterm : t -> preterm option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_preterm". +Ltac2 @ external of_preterm : preterm -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_of_preterm". +Ltac2 @ external to_preterm : t -> preterm option := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_to_preterm". -Ltac2 @ external of_ident : ident -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_ident". -Ltac2 @ external to_ident : t -> ident option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_ident". +Ltac2 @ external of_ident : ident -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_of_ident". +Ltac2 @ external to_ident : t -> ident option := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_to_ident". -Ltac2 @ external of_list : t list -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_list". -Ltac2 @ external to_list : t -> t list option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_list". +Ltac2 @ external of_list : t list -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_of_list". +Ltac2 @ external to_list : t -> t list option := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_to_list". -Ltac2 @ external of_intro_pattern : intro_pattern -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_intro_pattern". -Ltac2 @ external to_intro_pattern : t -> intro_pattern option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_intro_pattern". +Ltac2 @ external of_intro_pattern : intro_pattern -> t := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_of_intro_pattern". +Ltac2 @ external to_intro_pattern : t -> intro_pattern option := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_to_intro_pattern". (** Debug information *) -Ltac2 @ external tag_name : t -> string := "coq-core.plugins.ltac2_ltac1" "ltac1_tag_name". +Ltac2 @ external tag_name : t -> string := "rocq-runtime.plugins.ltac2_ltac1" "ltac1_tag_name". (** Name of the ltac1 value class the argument belongs to. Should be used only for error printing, typically "expected a constr but got a $tag_name". *) diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v index 626f1d9e582b..133b498f64ef 100644 --- a/user-contrib/Ltac2/Message.v +++ b/user-contrib/Ltac2/Message.v @@ -10,55 +10,55 @@ Require Import Ltac2.Init. -Ltac2 @ external print : message -> unit := "coq-core.plugins.ltac2" "print". +Ltac2 @ external print : message -> unit := "rocq-runtime.plugins.ltac2" "print". -Ltac2 @ external of_string : string -> message := "coq-core.plugins.ltac2" "message_of_string". +Ltac2 @ external of_string : string -> message := "rocq-runtime.plugins.ltac2" "message_of_string". -Ltac2 @ external to_string : message -> string := "coq-core.plugins.ltac2" "message_to_string". +Ltac2 @ external to_string : message -> string := "rocq-runtime.plugins.ltac2" "message_to_string". -Ltac2 @ external of_int : int -> message := "coq-core.plugins.ltac2" "message_of_int". +Ltac2 @ external of_int : int -> message := "rocq-runtime.plugins.ltac2" "message_of_int". -Ltac2 @ external of_ident : ident -> message := "coq-core.plugins.ltac2" "message_of_ident". +Ltac2 @ external of_ident : ident -> message := "rocq-runtime.plugins.ltac2" "message_of_ident". -Ltac2 @ external of_constr : constr -> message := "coq-core.plugins.ltac2" "message_of_constr". +Ltac2 @ external of_constr : constr -> message := "rocq-runtime.plugins.ltac2" "message_of_constr". (** Panics if there is more than one goal under focus. *) -Ltac2 @ external of_exn : exn -> message := "coq-core.plugins.ltac2" "message_of_exn". +Ltac2 @ external of_exn : exn -> message := "rocq-runtime.plugins.ltac2" "message_of_exn". (** Panics if there is more than one goal under focus. *) -Ltac2 @ external concat : message -> message -> message := "coq-core.plugins.ltac2" "message_concat". +Ltac2 @ external concat : message -> message -> message := "rocq-runtime.plugins.ltac2" "message_concat". (** Boxing primitives. They are translated to OCaml "Format" boxes, see https://ocaml.org/docs/formatting-text **) -Ltac2 @external force_new_line : message := "coq-core.plugins.ltac2" "message_force_new_line". +Ltac2 @external force_new_line : message := "rocq-runtime.plugins.ltac2" "message_force_new_line". (** Force writing on a new line after this. Warning: partially reinitialises the pretty-printing engine, potentially leading to bad printing afterwards. Prefer using a break hint inside a vertical box. *) -Ltac2 @external break : int -> int -> message := "coq-core.plugins.ltac2" "message_break". +Ltac2 @external break : int -> int -> message := "rocq-runtime.plugins.ltac2" "message_break". (** General break hint: [break n i] either prints [n] spaces or splits the line adding [i] to the current indentation. *) -Ltac2 @external space : message := "coq-core.plugins.ltac2" "message_space". +Ltac2 @external space : message := "rocq-runtime.plugins.ltac2" "message_space". (** Breaking space. Equivalent to [break 1 0]. *) -Ltac2 @external hbox : message -> message := "coq-core.plugins.ltac2" "message_hbox". +Ltac2 @external hbox : message -> message := "rocq-runtime.plugins.ltac2" "message_hbox". (** Horizontal box. Break hints in a horizontal box never split the line (nested boxes inside the horizontal box may allow line splitting). *) -Ltac2 @external vbox : int -> message -> message := "coq-core.plugins.ltac2" "message_vbox". +Ltac2 @external vbox : int -> message -> message := "rocq-runtime.plugins.ltac2" "message_vbox". (** Vertical box. Every break hint in a vertical box splits the line. The [int] is added to the current indentation when splitting the line. *) -Ltac2 @external hvbox : int -> message -> message := "coq-core.plugins.ltac2" "message_hvbox". +Ltac2 @external hvbox : int -> message -> message := "rocq-runtime.plugins.ltac2" "message_hvbox". (** Horizontal/vertical box. Behaves as a horizontal box if it fits on a single line, otherwise behaves as a vertical box (using the given [int]). *) -Ltac2 @external hovbox : int -> message -> message := "coq-core.plugins.ltac2" "message_hovbox". +Ltac2 @external hovbox : int -> message -> message := "rocq-runtime.plugins.ltac2" "message_hovbox". (** Horizonal-or-vertical box. Prints as much as possible on each line, splitting the line at break hints when there is no more room on the line (see "Printing Width" option). The [int] is added to @@ -68,30 +68,30 @@ Module Format. (** Only for internal use. *) -Ltac2 @ external stop : ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop". +Ltac2 @ external stop : ('a, 'b, 'c, 'a) format := "rocq-runtime.plugins.ltac2" "format_stop". Ltac2 @ external string : ('a, 'b, 'c, 'd) format -> - (string -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_string". + (string -> 'a, 'b, 'c, 'd) format := "rocq-runtime.plugins.ltac2" "format_string". Ltac2 @ external int : ('a, 'b, 'c, 'd) format -> - (int -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_int". + (int -> 'a, 'b, 'c, 'd) format := "rocq-runtime.plugins.ltac2" "format_int". Ltac2 @ external constr : ('a, 'b, 'c, 'd) format -> - (constr -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_constr". + (constr -> 'a, 'b, 'c, 'd) format := "rocq-runtime.plugins.ltac2" "format_constr". Ltac2 @ external ident : ('a, 'b, 'c, 'd) format -> - (ident -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_ident". + (ident -> 'a, 'b, 'c, 'd) format := "rocq-runtime.plugins.ltac2" "format_ident". Ltac2 @ external literal : string -> ('a, 'b, 'c, 'd) format -> - ('a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_literal". + ('a, 'b, 'c, 'd) format := "rocq-runtime.plugins.ltac2" "format_literal". Ltac2 @ external alpha : ('a, 'b, 'c, 'd) format -> - (('b -> 'r -> 'c) -> 'r -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_alpha". + (('b -> 'r -> 'c) -> 'r -> 'a, 'b, 'c, 'd) format := "rocq-runtime.plugins.ltac2" "format_alpha". Ltac2 @ external kfprintf : (message -> 'r) -> ('a, unit, message, 'r) format -> 'a := - "coq-core.plugins.ltac2" "format_kfprintf". + "rocq-runtime.plugins.ltac2" "format_kfprintf". Ltac2 @ external ikfprintf : ('v -> 'r) -> 'v -> ('a, unit, 'v, 'r) format -> 'a := - "coq-core.plugins.ltac2" "format_ikfprintf". + "rocq-runtime.plugins.ltac2" "format_ikfprintf". End Format. diff --git a/user-contrib/Ltac2/Meta.v b/user-contrib/Ltac2/Meta.v index 2cef130f1ae9..a84ac773156b 100644 --- a/user-contrib/Ltac2/Meta.v +++ b/user-contrib/Ltac2/Meta.v @@ -12,4 +12,4 @@ Require Import Ltac2.Init. Ltac2 Type t := meta. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "meta_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "meta_equal". diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v index f07a16d556b0..dbb3f159e367 100644 --- a/user-contrib/Ltac2/Pattern.v +++ b/user-contrib/Ltac2/Pattern.v @@ -21,16 +21,16 @@ Ltac2 Type match_kind := [ ]. Ltac2 @ external empty_context : context := - "coq-core.plugins.ltac2" "pattern_empty_context". + "rocq-runtime.plugins.ltac2" "pattern_empty_context". (** A trivial context only made of the hole. *) Ltac2 @ external matches : t -> constr -> (ident * constr) list := - "coq-core.plugins.ltac2" "pattern_matches". + "rocq-runtime.plugins.ltac2" "pattern_matches". (** If the term matches the pattern, returns the bound variables. If it doesn't, fail with [Match_failure]. Panics if not focused. *) Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) := - "coq-core.plugins.ltac2" "pattern_matches_subterm". + "rocq-runtime.plugins.ltac2" "pattern_matches_subterm". (** Returns a stream of results corresponding to all of the subterms of the term that matches the pattern as in [matches]. The stream is encoded as a backtracking value whose last exception is [Match_failure]. The additional @@ -38,11 +38,11 @@ Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) li the instantiate function. *) Ltac2 @ external matches_vect : t -> constr -> constr array := - "coq-core.plugins.ltac2" "pattern_matches_vect". + "rocq-runtime.plugins.ltac2" "pattern_matches_vect". (** Internal version of [matches] that does not return the identifiers. *) Ltac2 @ external matches_subterm_vect : t -> constr -> context * constr array := - "coq-core.plugins.ltac2" "pattern_matches_subterm_vect". + "rocq-runtime.plugins.ltac2" "pattern_matches_subterm_vect". (** Internal version of [matches_subterms] that does not return the identifiers. *) Ltac2 @ external matches_goal : @@ -50,7 +50,7 @@ Ltac2 @ external matches_goal : ((match_kind * t) option * (match_kind * t)) list -> (match_kind * t) -> ident array * context array * context array * constr array * context := - "coq-core.plugins.ltac2" "pattern_matches_goal". + "rocq-runtime.plugins.ltac2" "pattern_matches_goal". (** Given a list of patterns [hpats] for hypotheses and one pattern [cpat] for the conclusion, [matches_goal rev hpats cpat] produces (a stream of) tuples of: - An array of idents, whose size is the length of [hpats], corresponding to the @@ -72,7 +72,7 @@ Ltac2 @ external matches_goal : *) Ltac2 @ external instantiate : context -> constr -> constr := - "coq-core.plugins.ltac2" "pattern_instantiate". + "rocq-runtime.plugins.ltac2" "pattern_instantiate". (** Fill the hole of a context with the given term. *) (** Implementation of Ltac matching over terms and goals *) diff --git a/user-contrib/Ltac2/Proj.v b/user-contrib/Ltac2/Proj.v index 78b9f14cf30d..2ea0eafa622a 100644 --- a/user-contrib/Ltac2/Proj.v +++ b/user-contrib/Ltac2/Proj.v @@ -13,30 +13,30 @@ Require Import Ltac2.Init. Ltac2 Type t := projection. (** Type of primitive projections. This includes the unfolding boolean. *) -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "projection_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "projection_equal". (** Projections obtained through module aliases or Include are not considered equal by this function. The unfolding boolean is not ignored. *) -Ltac2 @ external ind : t -> inductive := "coq-core.plugins.ltac2" "projection_ind". +Ltac2 @ external ind : t -> inductive := "rocq-runtime.plugins.ltac2" "projection_ind". (** Get the inductive to which the projectin belongs. *) -Ltac2 @ external index : t -> int := "coq-core.plugins.ltac2" "projection_index". +Ltac2 @ external index : t -> int := "rocq-runtime.plugins.ltac2" "projection_index". (** The index of the projection indicates which field it projects. *) -Ltac2 @ external unfolded : t -> bool := "coq-core.plugins.ltac2" "projection_unfolded". +Ltac2 @ external unfolded : t -> bool := "rocq-runtime.plugins.ltac2" "projection_unfolded". (** Get the unfolding boolean. *) Ltac2 @ external set_unfolded : t -> bool -> t - := "coq-core.plugins.ltac2" "projection_set_unfolded". + := "rocq-runtime.plugins.ltac2" "projection_set_unfolded". (** Set the unfolding boolean. *) Ltac2 @ external of_constant : constant -> t option - := "coq-core.plugins.ltac2" "projection_of_constant". + := "rocq-runtime.plugins.ltac2" "projection_of_constant". (** Get the primitive projection associated to the constant. The returned projection is folded. Returns [None] when the constant is not associated to a primitive projection. *) Ltac2 @ external to_constant : t -> constant option - := "coq-core.plugins.ltac2" "projection_to_constant". + := "rocq-runtime.plugins.ltac2" "projection_to_constant". (** Get the constant associated to the primitive projection. Currently always returns [Some] but this may change in the future. *) diff --git a/user-contrib/Ltac2/Pstring.v b/user-contrib/Ltac2/Pstring.v index 204b9265f786..dfc4b4fac8fd 100644 --- a/user-contrib/Ltac2/Pstring.v +++ b/user-contrib/Ltac2/Pstring.v @@ -14,16 +14,16 @@ Ltac2 Type t := pstring. Ltac2 Type char63 := uint63. -Ltac2 @ external max_length : uint63 := "coq-core.plugins.ltac2" "pstring_max_length". +Ltac2 @ external max_length : uint63 := "rocq-runtime.plugins.ltac2" "pstring_max_length". -Ltac2 @ external to_string : t -> string := "coq-core.plugins.ltac2" "pstring_to_string". -Ltac2 @ external of_string : string -> t option := "coq-core.plugins.ltac2" "pstring_of_string". +Ltac2 @ external to_string : t -> string := "rocq-runtime.plugins.ltac2" "pstring_to_string". +Ltac2 @ external of_string : string -> t option := "rocq-runtime.plugins.ltac2" "pstring_of_string". -Ltac2 @ external make : uint63 -> char63 -> t := "coq-core.plugins.ltac2" "pstring_make". -Ltac2 @ external length : t -> uint63 := "coq-core.plugins.ltac2" "pstring_length". -Ltac2 @ external get : t -> uint63 -> char63 := "coq-core.plugins.ltac2" "pstring_get". -Ltac2 @ external sub : t -> uint63 -> uint63 -> t := "coq-core.plugins.ltac2" "pstring_sub". -Ltac2 @ external cat : t -> t -> t := "coq-core.plugins.ltac2" "pstring_cat". +Ltac2 @ external make : uint63 -> char63 -> t := "rocq-runtime.plugins.ltac2" "pstring_make". +Ltac2 @ external length : t -> uint63 := "rocq-runtime.plugins.ltac2" "pstring_length". +Ltac2 @ external get : t -> uint63 -> char63 := "rocq-runtime.plugins.ltac2" "pstring_get". +Ltac2 @ external sub : t -> uint63 -> uint63 -> t := "rocq-runtime.plugins.ltac2" "pstring_sub". +Ltac2 @ external cat : t -> t -> t := "rocq-runtime.plugins.ltac2" "pstring_cat". -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "pstring_equal". -Ltac2 @ external compare : t -> t -> int := "coq-core.plugins.ltac2" "pstring_compare". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "pstring_equal". +Ltac2 @ external compare : t -> t -> int := "rocq-runtime.plugins.ltac2" "pstring_compare". diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v index 9e0442a180f2..1ebd92c6d7bc 100644 --- a/user-contrib/Ltac2/Std.v +++ b/user-contrib/Ltac2/Std.v @@ -131,123 +131,123 @@ Ltac2 Type inversion_kind := [ (** Standard, built-in tactics. See Ltac1 for documentation. *) -Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "coq-core.plugins.ltac2" "tac_intros". +Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "rocq-runtime.plugins.ltac2" "tac_intros". Ltac2 @ external apply : advanced_flag -> evar_flag -> - (unit -> constr_with_bindings) list -> (ident * (intro_pattern option)) option -> unit := "coq-core.plugins.ltac2" "tac_apply". + (unit -> constr_with_bindings) list -> (ident * (intro_pattern option)) option -> unit := "rocq-runtime.plugins.ltac2" "tac_apply". -Ltac2 @ external elim : evar_flag -> constr_with_bindings -> constr_with_bindings option -> unit := "coq-core.plugins.ltac2" "tac_elim". -Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "coq-core.plugins.ltac2" "tac_case". +Ltac2 @ external elim : evar_flag -> constr_with_bindings -> constr_with_bindings option -> unit := "rocq-runtime.plugins.ltac2" "tac_elim". +Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "rocq-runtime.plugins.ltac2" "tac_case". -Ltac2 @ external generalize : (constr * occurrences * ident option) list -> unit := "coq-core.plugins.ltac2" "tac_generalize". +Ltac2 @ external generalize : (constr * occurrences * ident option) list -> unit := "rocq-runtime.plugins.ltac2" "tac_generalize". -Ltac2 @ external assert : assertion -> unit := "coq-core.plugins.ltac2" "tac_assert". -Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "coq-core.plugins.ltac2" "tac_enough". +Ltac2 @ external assert : assertion -> unit := "rocq-runtime.plugins.ltac2" "tac_assert". +Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "rocq-runtime.plugins.ltac2" "tac_enough". -Ltac2 @ external pose : ident option -> constr -> unit := "coq-core.plugins.ltac2" "tac_pose". -Ltac2 @ external set : evar_flag -> (unit -> ident option * constr) -> clause -> unit := "coq-core.plugins.ltac2" "tac_set". +Ltac2 @ external pose : ident option -> constr -> unit := "rocq-runtime.plugins.ltac2" "tac_pose". +Ltac2 @ external set : evar_flag -> (unit -> ident option * constr) -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_set". -Ltac2 @ external remember : evar_flag -> ident option -> (unit -> constr) -> intro_pattern option -> clause -> unit := "coq-core.plugins.ltac2" "tac_remember". +Ltac2 @ external remember : evar_flag -> ident option -> (unit -> constr) -> intro_pattern option -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_remember". Ltac2 @ external destruct : evar_flag -> induction_clause list -> - constr_with_bindings option -> unit := "coq-core.plugins.ltac2" "tac_destruct". + constr_with_bindings option -> unit := "rocq-runtime.plugins.ltac2" "tac_destruct". Ltac2 @ external induction : evar_flag -> induction_clause list -> - constr_with_bindings option -> unit := "coq-core.plugins.ltac2" "tac_induction". + constr_with_bindings option -> unit := "rocq-runtime.plugins.ltac2" "tac_induction". -Ltac2 @ external red : clause -> unit := "coq-core.plugins.ltac2" "tac_red". -Ltac2 @ external hnf : clause -> unit := "coq-core.plugins.ltac2" "tac_hnf". -Ltac2 @ external simpl : red_flags -> (pattern * occurrences) option -> clause -> unit := "coq-core.plugins.ltac2" "tac_simpl". -Ltac2 @ external cbv : red_flags -> clause -> unit := "coq-core.plugins.ltac2" "tac_cbv". -Ltac2 @ external cbn : red_flags -> clause -> unit := "coq-core.plugins.ltac2" "tac_cbn". -Ltac2 @ external lazy : red_flags -> clause -> unit := "coq-core.plugins.ltac2" "tac_lazy". -Ltac2 @ external unfold : (reference * occurrences) list -> clause -> unit := "coq-core.plugins.ltac2" "tac_unfold". -Ltac2 @ external fold : constr list -> clause -> unit := "coq-core.plugins.ltac2" "tac_fold". -Ltac2 @ external pattern : (constr * occurrences) list -> clause -> unit := "coq-core.plugins.ltac2" "tac_pattern". -Ltac2 @ external vm : (pattern * occurrences) option -> clause -> unit := "coq-core.plugins.ltac2" "tac_vm". -Ltac2 @ external native : (pattern * occurrences) option -> clause -> unit := "coq-core.plugins.ltac2" "tac_native". +Ltac2 @ external red : clause -> unit := "rocq-runtime.plugins.ltac2" "tac_red". +Ltac2 @ external hnf : clause -> unit := "rocq-runtime.plugins.ltac2" "tac_hnf". +Ltac2 @ external simpl : red_flags -> (pattern * occurrences) option -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_simpl". +Ltac2 @ external cbv : red_flags -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_cbv". +Ltac2 @ external cbn : red_flags -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_cbn". +Ltac2 @ external lazy : red_flags -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_lazy". +Ltac2 @ external unfold : (reference * occurrences) list -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_unfold". +Ltac2 @ external fold : constr list -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_fold". +Ltac2 @ external pattern : (constr * occurrences) list -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_pattern". +Ltac2 @ external vm : (pattern * occurrences) option -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_vm". +Ltac2 @ external native : (pattern * occurrences) option -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_native". -Ltac2 @ external eval_red : constr -> constr := "coq-core.plugins.ltac2" "eval_red". -Ltac2 @ external eval_hnf : constr -> constr := "coq-core.plugins.ltac2" "eval_hnf". -Ltac2 @ external eval_red : constr -> constr := "coq-core.plugins.ltac2" "eval_red". -Ltac2 @ external eval_simpl : red_flags -> (pattern * occurrences) option -> constr -> constr := "coq-core.plugins.ltac2" "eval_simpl". -Ltac2 @ external eval_cbv : red_flags -> constr -> constr := "coq-core.plugins.ltac2" "eval_cbv". -Ltac2 @ external eval_cbn : red_flags -> constr -> constr := "coq-core.plugins.ltac2" "eval_cbn". -Ltac2 @ external eval_lazy : red_flags -> constr -> constr := "coq-core.plugins.ltac2" "eval_lazy". -Ltac2 @ external eval_unfold : (reference * occurrences) list -> constr -> constr := "coq-core.plugins.ltac2" "eval_unfold". -Ltac2 @ external eval_fold : constr list -> constr -> constr := "coq-core.plugins.ltac2" "eval_fold". -Ltac2 @ external eval_pattern : (constr * occurrences) list -> constr -> constr := "coq-core.plugins.ltac2" "eval_pattern". -Ltac2 @ external eval_vm : (pattern * occurrences) option -> constr -> constr := "coq-core.plugins.ltac2" "eval_vm". -Ltac2 @ external eval_native : (pattern * occurrences) option -> constr -> constr := "coq-core.plugins.ltac2" "eval_native". +Ltac2 @ external eval_red : constr -> constr := "rocq-runtime.plugins.ltac2" "eval_red". +Ltac2 @ external eval_hnf : constr -> constr := "rocq-runtime.plugins.ltac2" "eval_hnf". +Ltac2 @ external eval_red : constr -> constr := "rocq-runtime.plugins.ltac2" "eval_red". +Ltac2 @ external eval_simpl : red_flags -> (pattern * occurrences) option -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_simpl". +Ltac2 @ external eval_cbv : red_flags -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_cbv". +Ltac2 @ external eval_cbn : red_flags -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_cbn". +Ltac2 @ external eval_lazy : red_flags -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_lazy". +Ltac2 @ external eval_unfold : (reference * occurrences) list -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_unfold". +Ltac2 @ external eval_fold : constr list -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_fold". +Ltac2 @ external eval_pattern : (constr * occurrences) list -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_pattern". +Ltac2 @ external eval_vm : (pattern * occurrences) option -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_vm". +Ltac2 @ external eval_native : (pattern * occurrences) option -> constr -> constr := "rocq-runtime.plugins.ltac2" "eval_native". -Ltac2 @ external change : pattern option -> (constr array -> constr) -> clause -> unit := "coq-core.plugins.ltac2" "tac_change". +Ltac2 @ external change : pattern option -> (constr array -> constr) -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_change". -Ltac2 @ external rewrite : evar_flag -> rewriting list -> clause -> (unit -> unit) option -> unit := "coq-core.plugins.ltac2" "tac_rewrite". +Ltac2 @ external rewrite : evar_flag -> rewriting list -> clause -> (unit -> unit) option -> unit := "rocq-runtime.plugins.ltac2" "tac_rewrite". -Ltac2 @ external setoid_rewrite : orientation -> (unit -> constr_with_bindings) -> occurrences -> ident option -> unit := "coq-core.plugins.ltac2" "tac_setoid_rewrite". +Ltac2 @ external setoid_rewrite : orientation -> (unit -> constr_with_bindings) -> occurrences -> ident option -> unit := "rocq-runtime.plugins.ltac2" "tac_setoid_rewrite". -Ltac2 @ external reflexivity : unit -> unit := "coq-core.plugins.ltac2" "tac_reflexivity". +Ltac2 @ external reflexivity : unit -> unit := "rocq-runtime.plugins.ltac2" "tac_reflexivity". -Ltac2 @ external assumption : unit -> unit := "coq-core.plugins.ltac2" "tac_assumption". +Ltac2 @ external assumption : unit -> unit := "rocq-runtime.plugins.ltac2" "tac_assumption". -Ltac2 @ external transitivity : constr -> unit := "coq-core.plugins.ltac2" "tac_transitivity". +Ltac2 @ external transitivity : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_transitivity". -Ltac2 @ external etransitivity : unit -> unit := "coq-core.plugins.ltac2" "tac_etransitivity". +Ltac2 @ external etransitivity : unit -> unit := "rocq-runtime.plugins.ltac2" "tac_etransitivity". -Ltac2 @ external cut : constr -> unit := "coq-core.plugins.ltac2" "tac_cut". +Ltac2 @ external cut : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_cut". -Ltac2 @ external left : evar_flag -> bindings -> unit := "coq-core.plugins.ltac2" "tac_left". -Ltac2 @ external right : evar_flag -> bindings -> unit := "coq-core.plugins.ltac2" "tac_right". +Ltac2 @ external left : evar_flag -> bindings -> unit := "rocq-runtime.plugins.ltac2" "tac_left". +Ltac2 @ external right : evar_flag -> bindings -> unit := "rocq-runtime.plugins.ltac2" "tac_right". -Ltac2 @ external constructor : evar_flag -> unit := "coq-core.plugins.ltac2" "tac_constructor". -Ltac2 @ external split : evar_flag -> bindings -> unit := "coq-core.plugins.ltac2" "tac_split". +Ltac2 @ external constructor : evar_flag -> unit := "rocq-runtime.plugins.ltac2" "tac_constructor". +Ltac2 @ external split : evar_flag -> bindings -> unit := "rocq-runtime.plugins.ltac2" "tac_split". -Ltac2 @ external constructor_n : evar_flag -> int -> bindings -> unit := "coq-core.plugins.ltac2" "tac_constructorn". +Ltac2 @ external constructor_n : evar_flag -> int -> bindings -> unit := "rocq-runtime.plugins.ltac2" "tac_constructorn". -Ltac2 @ external intros_until : hypothesis -> unit := "coq-core.plugins.ltac2" "tac_introsuntil". +Ltac2 @ external intros_until : hypothesis -> unit := "rocq-runtime.plugins.ltac2" "tac_introsuntil". -Ltac2 @ external symmetry : clause -> unit := "coq-core.plugins.ltac2" "tac_symmetry". +Ltac2 @ external symmetry : clause -> unit := "rocq-runtime.plugins.ltac2" "tac_symmetry". -Ltac2 @ external rename : (ident * ident) list -> unit := "coq-core.plugins.ltac2" "tac_rename". +Ltac2 @ external rename : (ident * ident) list -> unit := "rocq-runtime.plugins.ltac2" "tac_rename". -Ltac2 @ external revert : ident list -> unit := "coq-core.plugins.ltac2" "tac_revert". +Ltac2 @ external revert : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_revert". -Ltac2 @ external admit : unit -> unit := "coq-core.plugins.ltac2" "tac_admit". +Ltac2 @ external admit : unit -> unit := "rocq-runtime.plugins.ltac2" "tac_admit". -Ltac2 @ external fix_ : ident -> int -> unit := "coq-core.plugins.ltac2" "tac_fix". -Ltac2 @ external cofix_ : ident -> unit := "coq-core.plugins.ltac2" "tac_cofix". +Ltac2 @ external fix_ : ident -> int -> unit := "rocq-runtime.plugins.ltac2" "tac_fix". +Ltac2 @ external cofix_ : ident -> unit := "rocq-runtime.plugins.ltac2" "tac_cofix". -Ltac2 @ external clear : ident list -> unit := "coq-core.plugins.ltac2" "tac_clear". -Ltac2 @ external keep : ident list -> unit := "coq-core.plugins.ltac2" "tac_keep". +Ltac2 @ external clear : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_clear". +Ltac2 @ external keep : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_keep". -Ltac2 @ external clearbody : ident list -> unit := "coq-core.plugins.ltac2" "tac_clearbody". +Ltac2 @ external clearbody : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_clearbody". -Ltac2 @ external exact_no_check : constr -> unit := "coq-core.plugins.ltac2" "tac_exactnocheck". -Ltac2 @ external vm_cast_no_check : constr -> unit := "coq-core.plugins.ltac2" "tac_vmcastnocheck". -Ltac2 @ external native_cast_no_check : constr -> unit := "coq-core.plugins.ltac2" "tac_nativecastnocheck". +Ltac2 @ external exact_no_check : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_exactnocheck". +Ltac2 @ external vm_cast_no_check : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_vmcastnocheck". +Ltac2 @ external native_cast_no_check : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_nativecastnocheck". -Ltac2 @ external inversion : inversion_kind -> destruction_arg -> intro_pattern option -> ident list option -> unit := "coq-core.plugins.ltac2" "tac_inversion". +Ltac2 @ external inversion : inversion_kind -> destruction_arg -> intro_pattern option -> ident list option -> unit := "rocq-runtime.plugins.ltac2" "tac_inversion". (** coretactics *) -Ltac2 @ external move : ident -> move_location -> unit := "coq-core.plugins.ltac2" "tac_move". +Ltac2 @ external move : ident -> move_location -> unit := "rocq-runtime.plugins.ltac2" "tac_move". -Ltac2 @ external intro : ident option -> move_location option -> unit := "coq-core.plugins.ltac2" "tac_intro". +Ltac2 @ external intro : ident option -> move_location option -> unit := "rocq-runtime.plugins.ltac2" "tac_intro". -Ltac2 @ external specialize : constr_with_bindings -> intro_pattern option -> unit := "coq-core.plugins.ltac2" "tac_specialize". +Ltac2 @ external specialize : constr_with_bindings -> intro_pattern option -> unit := "rocq-runtime.plugins.ltac2" "tac_specialize". (** extratactics *) -Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "coq-core.plugins.ltac2" "tac_discriminate". -Ltac2 @ external injection : evar_flag -> intro_pattern list option -> destruction_arg option -> unit := "coq-core.plugins.ltac2" "tac_injection". +Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "rocq-runtime.plugins.ltac2" "tac_discriminate". +Ltac2 @ external injection : evar_flag -> intro_pattern list option -> destruction_arg option -> unit := "rocq-runtime.plugins.ltac2" "tac_injection". -Ltac2 @ external absurd : constr -> unit := "coq-core.plugins.ltac2" "tac_absurd". -Ltac2 @ external contradiction : constr_with_bindings option -> unit := "coq-core.plugins.ltac2" "tac_contradiction". +Ltac2 @ external absurd : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_absurd". +Ltac2 @ external contradiction : constr_with_bindings option -> unit := "rocq-runtime.plugins.ltac2" "tac_contradiction". -Ltac2 @ external autorewrite : bool -> (unit -> unit) option -> ident list -> clause -> unit := "coq-core.plugins.ltac2" "tac_autorewrite". +Ltac2 @ external autorewrite : bool -> (unit -> unit) option -> ident list -> clause -> unit := "rocq-runtime.plugins.ltac2" "tac_autorewrite". -Ltac2 @ external subst : ident list -> unit := "coq-core.plugins.ltac2" "tac_subst". -Ltac2 @ external subst_all : unit -> unit := "coq-core.plugins.ltac2" "tac_substall". +Ltac2 @ external subst : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_subst". +Ltac2 @ external subst_all : unit -> unit := "rocq-runtime.plugins.ltac2" "tac_substall". (** auto *) @@ -255,23 +255,23 @@ Ltac2 Type debug := [ Off | Info | Debug ]. Ltac2 Type strategy := [ BFS | DFS ]. -Ltac2 @ external trivial : debug -> reference list -> ident list option -> unit := "coq-core.plugins.ltac2" "tac_trivial". +Ltac2 @ external trivial : debug -> reference list -> ident list option -> unit := "rocq-runtime.plugins.ltac2" "tac_trivial". -Ltac2 @ external auto : debug -> int option -> reference list -> ident list option -> unit := "coq-core.plugins.ltac2" "tac_auto". +Ltac2 @ external auto : debug -> int option -> reference list -> ident list option -> unit := "rocq-runtime.plugins.ltac2" "tac_auto". -Ltac2 @ external eauto : debug -> int option -> reference list -> ident list option -> unit := "coq-core.plugins.ltac2" "tac_eauto". +Ltac2 @ external eauto : debug -> int option -> reference list -> ident list option -> unit := "rocq-runtime.plugins.ltac2" "tac_eauto". -Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "coq-core.plugins.ltac2" "tac_typeclasses_eauto". +Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "rocq-runtime.plugins.ltac2" "tac_typeclasses_eauto". -Ltac2 @ external resolve_tc : constr -> unit := "coq-core.plugins.ltac2" "tac_resolve_tc". +Ltac2 @ external resolve_tc : constr -> unit := "rocq-runtime.plugins.ltac2" "tac_resolve_tc". (** Resolve the existential variables appearing in the constr whose types are typeclasses. Fail if any of them cannot be resolved. Does not focus. *) -Ltac2 @ external unify : constr -> constr -> unit := "coq-core.plugins.ltac2" "tac_unify". +Ltac2 @ external unify : constr -> constr -> unit := "rocq-runtime.plugins.ltac2" "tac_unify". Ltac2 @ external congruence : int option -> constr list option -> unit := - "coq-core.plugins.ltac2" "congruence". + "rocq-runtime.plugins.ltac2" "congruence". Ltac2 @ external simple_congruence : int option -> constr list option -> unit := - "coq-core.plugins.ltac2" "simple_congruence". + "rocq-runtime.plugins.ltac2" "simple_congruence". diff --git a/user-contrib/Ltac2/String.v b/user-contrib/Ltac2/String.v index af664ad5bc9e..14de5dff7aea 100644 --- a/user-contrib/Ltac2/String.v +++ b/user-contrib/Ltac2/String.v @@ -12,14 +12,14 @@ Require Import Ltac2.Init. Ltac2 Type t := string. -Ltac2 @external make : int -> char -> string := "coq-core.plugins.ltac2" "string_make". -Ltac2 @external length : string -> int := "coq-core.plugins.ltac2" "string_length". -Ltac2 @external get : string -> int -> char := "coq-core.plugins.ltac2" "string_get". -Ltac2 @external set : string -> int -> char -> unit := "coq-core.plugins.ltac2" "string_set". -Ltac2 @external concat : string -> string list -> string := "coq-core.plugins.ltac2" "string_concat". -Ltac2 @external app : string -> string -> string := "coq-core.plugins.ltac2" "string_app". -Ltac2 @external sub : string -> int -> int -> string := "coq-core.plugins.ltac2" "string_sub". -Ltac2 @external equal : string -> string -> bool := "coq-core.plugins.ltac2" "string_equal". -Ltac2 @external compare : string -> string -> int := "coq-core.plugins.ltac2" "string_compare". +Ltac2 @external make : int -> char -> string := "rocq-runtime.plugins.ltac2" "string_make". +Ltac2 @external length : string -> int := "rocq-runtime.plugins.ltac2" "string_length". +Ltac2 @external get : string -> int -> char := "rocq-runtime.plugins.ltac2" "string_get". +Ltac2 @external set : string -> int -> char -> unit := "rocq-runtime.plugins.ltac2" "string_set". +Ltac2 @external concat : string -> string list -> string := "rocq-runtime.plugins.ltac2" "string_concat". +Ltac2 @external app : string -> string -> string := "rocq-runtime.plugins.ltac2" "string_app". +Ltac2 @external sub : string -> int -> int -> string := "rocq-runtime.plugins.ltac2" "string_sub". +Ltac2 @external equal : string -> string -> bool := "rocq-runtime.plugins.ltac2" "string_equal". +Ltac2 @external compare : string -> string -> int := "rocq-runtime.plugins.ltac2" "string_compare". Ltac2 is_empty s := match s with "" => true | _ => false end. diff --git a/user-contrib/Ltac2/TransparentState.v b/user-contrib/Ltac2/TransparentState.v index fbb0b77e41b7..20cfdba2e8bd 100644 --- a/user-contrib/Ltac2/TransparentState.v +++ b/user-contrib/Ltac2/TransparentState.v @@ -15,13 +15,13 @@ Ltac2 Type t. (** [empty] is the empty transparency state (all constants are opaque). *) Ltac2 @ external empty : t := - "coq-core.plugins.ltac2" "empty_transparent_state". + "rocq-runtime.plugins.ltac2" "empty_transparent_state". (** [full] is the full transparency state (all constants are transparent). *) Ltac2 @ external full : t := - "coq-core.plugins.ltac2" "full_transparent_state". + "rocq-runtime.plugins.ltac2" "full_transparent_state". (** [current ()] gives the transparency state of the goal, which is influenced by, e.g., the [Strategy] command, or the [with_strategy] Ltac tactic. *) Ltac2 @ external current : unit -> t := - "coq-core.plugins.ltac2" "current_transparent_state". + "rocq-runtime.plugins.ltac2" "current_transparent_state". diff --git a/user-contrib/Ltac2/Uint63.v b/user-contrib/Ltac2/Uint63.v index 850a6d7585ad..a2efb845cbde 100644 --- a/user-contrib/Ltac2/Uint63.v +++ b/user-contrib/Ltac2/Uint63.v @@ -12,10 +12,10 @@ Require Import Ltac2.Init. Ltac2 Type t := uint63. -Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "uint63_equal". +Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "uint63_equal". -Ltac2 @external compare : t -> t -> int := "coq-core.plugins.ltac2" "uint63_compare". +Ltac2 @external compare : t -> t -> int := "rocq-runtime.plugins.ltac2" "uint63_compare". -Ltac2 @external of_int : int -> t := "coq-core.plugins.ltac2" "uint63_of_int". +Ltac2 @external of_int : int -> t := "rocq-runtime.plugins.ltac2" "uint63_of_int". -Ltac2 @external print : t -> message := "coq-core.plugins.ltac2" "uint63_print". +Ltac2 @external print : t -> message := "rocq-runtime.plugins.ltac2" "uint63_print". diff --git a/user-contrib/Ltac2/Unification.v b/user-contrib/Ltac2/Unification.v index 2b4802603ca0..1b3840f525fb 100644 --- a/user-contrib/Ltac2/Unification.v +++ b/user-contrib/Ltac2/Unification.v @@ -15,7 +15,7 @@ Require Ltac2.TransparentState. may have the effect of instantiating evars. If the [c1] and [c2] cannot be unified, an [Internal] exception is raised. *) Ltac2 @ external unify : TransparentState.t -> constr -> constr -> unit := - "coq-core.plugins.ltac2" "evarconv_unify". + "rocq-runtime.plugins.ltac2" "evarconv_unify". (** [unify_with_full_ts] is like [unify TransparentState.full]. *) Ltac2 unify_with_full_ts : constr -> constr -> unit := fun c1 c2 => diff --git a/user-contrib/Ltac2/dune.disabled b/user-contrib/Ltac2/dune.disabled index b1cc5fb7aeba..54594bcc61a4 100644 --- a/user-contrib/Ltac2/dune.disabled +++ b/user-contrib/Ltac2/dune.disabled @@ -4,5 +4,5 @@ (synopsis "Ltac2 tactic language") (flags -w -deprecated-native-compiler-option) (plugins - coq-core.plugins.ltac2_ltac1 - coq-core.plugins.ltac2)) + rocq-runtime.plugins.ltac2_ltac1 + rocq-runtime.plugins.ltac2)) diff --git a/vernac/dune b/vernac/dune index 48693330c165..49e32c9046d0 100644 --- a/vernac/dune +++ b/vernac/dune @@ -1,11 +1,15 @@ (library (name vernac) (synopsis "Coq's Vernacular Language") - (public_name coq-core.vernac) + (public_name rocq-runtime.vernac) (wrapped false) (modules_without_implementation vernacexpr) ; until ocaml/dune#4892 fixed ; (private_modules comProgramFixpoint egramcoq) (libraries tactics parsing findlib.dynload)) +(deprecated_library_name + (old_public_name coq-core.vernac) + (new_public_name rocq-runtime.vernac)) + (coq.pp (modules g_proofs g_vernac g_redexpr)) diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 1e42d0c01b18..477a71fc58d8 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -15,7 +15,7 @@ module PluginSpec : sig (** A plugin is identified by its canonical library name, - such as [coq-core.plugins.ltac] *) + such as [rocq-runtime.plugins.ltac] *) type t (** [to_package p] returns the findlib name of the package *) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 2409d712024a..e2080ac2553b 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -95,7 +95,7 @@ type ty_ml = TyML : bool (* deprecated *) * ('r, 's) ty_sig * 'r * 's option -> Commands added without providing [plugin] cannot be removed from the grammar or modified. Not passing [plugin] is possible for - non-plugin coq-core commands and deprecated for all other callers. + non-plugin rocq-runtime commands and deprecated for all other callers. *) val static_vernac_extend : plugin:string option ->