aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/nix/bignums.nix2
-rw-r--r--dev/ci/nix/unicoq/unicoq-num.patch31
-rw-r--r--dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh7
-rw-r--r--dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh6
-rw-r--r--dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh6
-rw-r--r--dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh6
-rw-r--r--dev/doc/changes.md7
-rw-r--r--dev/doc/release-process.md22
-rw-r--r--dev/include_printers1
-rw-r--r--dev/nixpkgs.nix4
-rw-r--r--dev/top_printers.dbg1
-rw-r--r--dev/top_printers.ml10
-rw-r--r--dev/top_printers.mli1
13 files changed, 66 insertions, 38 deletions
diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
index 1d931c858e..d813ddd8d7 100644
--- a/dev/ci/nix/bignums.nix
+++ b/dev/ci/nix/bignums.nix
@@ -1,5 +1,5 @@
{ ocamlPackages }:
{
- buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+ buildInputs = [ ocamlPackages.ocaml ];
}
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
index 6d96d94dfc..6d2f6470b1 100644
--- a/dev/ci/nix/unicoq/unicoq-num.patch
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -4,19 +4,6 @@ Date: Thu Nov 29 08:59:22 2018 +0000
Make explicit dependency to num
-diff --git a/Make b/Make
-index 550dc6a..8aa1309 100644
---- a/Make
-+++ b/Make
-@@ -9,7 +9,7 @@ src/logger.ml
- src/munify.mli
- src/munify.ml
- src/unitactics.mlg
--src/unicoq.mllib
-+src/unicoq.mlpack
- theories/Unicoq.v
- test-suite/munifytest.v
- test-suite/microtests.v
diff --git a/Makefile.local b/Makefile.local
new file mode 100644
index 0000000..88be365
@@ -24,21 +11,3 @@ index 0000000..88be365
+++ b/Makefile.local
@@ -0,0 +1 @@
+CAMLPKGS += -package num
-diff --git a/src/unicoq.mllib b/src/unicoq.mllib
-deleted file mode 100644
-index 2b84e2d..0000000
---- a/src/unicoq.mllib
-+++ /dev/null
-@@ -1,3 +0,0 @@
--Logger
--Munify
--Unitactics
-diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
-new file mode 100644
-index 0000000..2b84e2d
---- /dev/null
-+++ b/src/unicoq.mlpack
-@@ -0,0 +1,3 @@
-+Logger
-+Munify
-+Unitactics
diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
new file mode 100644
index 0000000000..dc39ea5ef0
--- /dev/null
+++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then
+
+ equations_CI_BRANCH=master+fix-evars_of_term-pr8893
+ equations_CI_REF=master+fix-evars_of_term-pr8893
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+ elpi_CI_REF=canonical-disable-hint
+ elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
new file mode 100644
index 0000000000..4032b1c6b5
--- /dev/null
+++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then
+
+ paramcoq_CI_REF=run_tactic_gen
+ paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
new file mode 100644
index 0000000000..bc8aa33565
--- /dev/null
+++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then
+
+ unicoq_CI_REF=detype-anonymous
+ unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9e0d47651e..7221c3de56 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,10 @@
+## Changes between Coq 8.10 and Coq 8.11
+
+### ML API
+
+- Functions and types deprecated in 8.10 have been removed in Coq
+ 8.11.
+
## Changes between Coq 8.9 and Coq 8.10
### ML4 Pre Processing
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 60c0886896..189d6f9fa5 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -84,10 +84,18 @@
Coq has been tagged.
- [ ] Have some people test the recently auto-generated Windows and MacOS
packages.
-- [ ] Change the version name from alpha to beta1 (see
+- [ ] In a PR:
+ - Change the version name from alpha to beta1 (see
[#7009](https://github.com/coq/coq/pull/7009/files)).
- We generally do not update the magic numbers at this point.
+ - We generally do not update the magic numbers at this point.
+ - Set `is_a_released_version` to `true` in `configure.ml`.
- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+- [ ] Check using `git push --tags --dry-run` that you are not
+ pushing anything else than the new tag. If needed, remove spurious
+ tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+ (if you forget about it, you'll be reminded whenever you try to
+ backport a PR with a changelog entry).
### These steps are the same for all releases (beta, final, patch-level) ###
@@ -112,9 +120,17 @@
## At the final release time ##
-- [ ] Change the version name to X.X.0 and the magic numbers (see
+- [ ] In a PR:
+ - Change the version name from X.X.0 and the magic numbers (see
[#7271](https://github.com/coq/coq/pull/7271/files)).
+ - Set `is_a_released_version` to `true` in `configure.ml`.
- [ ] Put the `VX.X.0` tag.
+- [ ] Check using `git push --tags --dry-run` that you are not
+ pushing anything else than the new tag. If needed, remove spurious
+ tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+ (if you forget about it, you'll be reminded whenever you try to
+ backport a PR with a changelog entry).
Repeat the generic process documented above for all releases.
diff --git a/dev/include_printers b/dev/include_printers
index 90088e40bf..d077075eeb 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -11,6 +11,7 @@
#install_printer (* universes *) ppuniverses;;
#install_printer (* univ level *) ppuni_level;;
#install_printer (* univ context *) ppuniverse_context;;
+#install_printer (* univ context *) ppaucontext;;
#install_printer (* univ context future *) ppuniverse_context_future;;
#install_printer (* univ context set *) ppuniverse_context_set;;
#install_printer (* univ set *) ppuniverse_set;;
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index f4786d9431..8dfe1e7833 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
import (fetchTarball {
- url = "https://github.com/NixOS/nixpkgs/archive/8471ab76242987b11afd4486b82888e1588f8307.tar.gz";
- sha256 = "06pp6b6x78jlinxifnphkbp79dx58jr990fkm4qziq0ay5klpxd7";
+ url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz";
+ sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1";
})
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index a6ecec7e33..82f2e79549 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level
install_printer Top_printers.ppuniverse_set
install_printer Top_printers.ppuniverse_instance
install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppaucontext
install_printer Top_printers.ppuniverse_context_set
install_printer Top_printers.ppuniverse_subst
install_printer Top_printers.ppuniverse_opt_subst
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 816316487c..2859b56cbe 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,7 +27,6 @@ open Clenv
let _ = Detyping.print_evar_arguments := true
let _ = Detyping.print_universes := true
let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
(* std_ppcmds *)
let pp x = Pp.pp_with !Topfmt.std_ft x
@@ -236,6 +235,15 @@ let ppnamedcontextval e =
let sigma = Evd.from_env env in
pp (pr_named_context env sigma (named_context_of_val e))
+let ppaucontext auctx =
+ let nas = AUContext.names auctx in
+ let prlev l = match Level.var_index l with
+ | Some n -> Name.print nas.(n)
+ | None -> prlev l
+ in
+ pp (pr_universe_context prlev (AUContext.repr auctx))
+
+
let ppenv e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index cb32d2294c..2aa1808322 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
val ppuniverse_set : Univ.LSet.t -> unit
val ppuniverse_instance : Univ.Instance.t -> unit
val ppuniverse_context : Univ.UContext.t -> unit
+val ppaucontext : Univ.AUContext.t -> unit
val ppuniverse_context_set : Univ.ContextSet.t -> unit
val ppuniverse_subst : Univ.universe_subst -> unit
val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 12:13:03 +0000