[vendor] [deps] Bump Coq

ejgallego · Mar 6, 2025 · e5d15c4 · e5d15c4
1 parent d9b5f11
commit e5d15c4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/vendor/coq b/vendor/coq
diff --git a/vendor/coq-stdlib b/vendor/coq-stdlib
+3 −2		checker/mod_checking.ml
+11 −0		dev/bench/benchUtil.ml
+11 −0		dev/bench/benchUtil.mli
+38 −15		dev/bench/htmloutput.ml
+3 −3		dev/bench/htmloutput.mli
+22 −9		dev/bench/profparser.ml
+1 −1		dev/bench/profparser.mli
+2 −2		dev/bench/timelog2html.ml
+1 −1		dev/ci/ci-basic-overlay.sh
+1 −1		dev/ci/scripts/ci-common.sh
+3 −0		dev/ci/user-overlays/20315-SkySkimmer-ltac-may-eval.sh
+1 −0		dev/top_printers.dbg
+2 −0		dev/top_printers.ml
+2 −0		dev/top_printers.mli
+5 −0		doc/changelog/06-Ltac2-language/20220-better-fresh.rst
+6 −8		engine/evd.ml
+4 −2		engine/evd.mli
+2 −0		engine/namegen.mli
+25 −0		engine/nameops.ml
+1 −0		engine/nameops.mli
+35 −34		interp/constrintern.ml
+33 −6		interp/notation.ml
+1 −1		interp/notation.mli
+1 −1		interp/notation_ops.ml
+6 −4		kernel/inductive.ml
+3 −1		kernel/inductive.mli
+1 −1		kernel/mod_subst.ml
+4 −0		kernel/safe_typing.ml
+2 −0		kernel/safe_typing.mli
+1 −1		kernel/typeops.ml
+11 −15		plugins/firstorder/formula.ml
+5 −3		plugins/firstorder/formula.mli
+3 −3		plugins/firstorder/ground.ml
+3 −1		plugins/firstorder/instances.ml
+46 −17		plugins/firstorder/rules.ml
+2 −2		plugins/firstorder/rules.mli
+27 −66		plugins/firstorder/sequent.ml
+2 −4		plugins/firstorder/sequent.mli
+0 −1		plugins/ltac/g_ltac.mlg
+0 −1		plugins/ltac/pltac.mli
+0 −1		plugins/ltac/pptactic.ml
+1 −1		plugins/ltac/pptactic.mli
+6 −0		plugins/ltac/tacexpr.mli
+0 −1		plugins/ltac/tacintern.ml
+0 −1		plugins/ltac/tacinterp.ml
+0 −1		plugins/ltac/tacsubst.ml
+17 −5		plugins/ltac2/tac2core.ml
+1 −1		plugins/ltac2/tac2ffi.ml
+3 −3		plugins/ltac2/tac2ffi.mli
+3 −0		plugins/ltac2/tac2stdlib.ml
+2 −0		plugins/ltac2/tac2tactics.ml
+2 −0		plugins/ltac2/tac2tactics.mli
+4 −2		plugins/ssr/ssrcommon.ml
+5 −2		plugins/ssr/ssrequality.ml
+1 −1		plugins/ssr/ssrvernac.mlg
+13 −6		pretyping/cases.ml
+6 −3		pretyping/coercion.ml
+2 −1		pretyping/combinators.ml
+5 −2		pretyping/evarconv.ml
+3 −1		pretyping/evardefine.ml
+2 −1		pretyping/evarsolve.ml
+10 −16		pretyping/globEnv.ml
+3 −4		pretyping/globEnv.mli
+33 −6		pretyping/indrec.ml
+0 −2		pretyping/typeclasses.ml
+2 −0		pretyping/typeclasses.mli
+1 −1		pretyping/typing.ml
+6 −3		pretyping/unification.ml
+4 −3		proofs/clenv.ml
+4 −2		proofs/proof.ml
+1 −2		proofs/refine.ml
+9 −3		tactics/btermdn.ml
+2 −1		tactics/evar_tactics.ml
+0 −6		tactics/genredexpr.mli
+4 −2		tactics/tactics.ml
+34 −0		test-suite/bugs/bug_16967_1.v
+26 −0		test-suite/bugs/bug_20301.v
+27 −0		test-suite/bugs/bug_20308.v
+3 −3		test-suite/output/Notations3.out
+2 −2		test-suite/output/PrintMatch.out
+1 −1		test-suite/output/UnivBinders.out
+2 −1		test-suite/output/bug_9180.out
+8 −8		test-suite/output/locate.out
+2 −2		test-suite/output/wish_17316.out
+13 −4		user-contrib/Ltac2/Fresh.v
+3 −2		user-contrib/Ltac2/Notations.v
+4 −0		user-contrib/Ltac2/Std.v
+2 −1		vernac/comFixpoint.ml
+2 −1		vernac/comInductive.ml
+13 −12		vernac/declare.ml
+177 −124		.github/workflows/nix-action-rocq-9.0.yml
+224 −148		.github/workflows/nix-action-rocq-master.yml
+2 −2		.gitignore
+28 −12		.nix/config.nix
+1 −1		.nix/coq-nix-toolbox.nix
+165 −0		.nix/coq-overlays/coq-elpi/default.nix
+2 −2		.nix/coq-overlays/fcsl-pcm/default.nix
+0 −12		.nix/coq-overlays/jasmin/default.nix
+7 −1		.nix/coq-overlays/stdlib-refman-html/default.nix
+48 −0		.nix/coq-overlays/trakt/default.nix
+6 −7		.nix/rocq-overlays/rocq-elpi-test/default.nix
+2 −2		.nix/rocq-overlays/stdlib-html/default.nix
+5 −5		.nix/rocq-overlays/stdlib-subcomponents/default.nix
+3 −8		.nix/rocq-overlays/stdlib-test/default.nix
+2 −2		default.nix
+2 −2		dev/doc/structure.md
+1 −0		doc/common/macros.tex
+119 −0		doc/sphinx/_static/coqdoc.css
+0 −1		doc/sphinx/conf.py
+2 −2		doc/sphinx/introduction.rst
+3 −3		doc/sphinx/language/coq-library.rst
+2 −2		doc/stdlib/Library.tex
+11 −2		test-suite/Makefile
+ −		test-suite/output/BinaryPrintingNotations.v
+1,110 −0		test-suite/output/StringSyntax.out.9.0
+1 −0		test-suite/output/allBytes.v
+21 −0		test-suite/output/bug_19702.out.9.0
+2 −0		theories/Makefile