Merge pull request #765 from ejgallego/bump_coq

[deps] [vendor] Bump Coq usptream
ejgallego · Jun 7, 2024 · c3a5da6 · c3a5da6
2 parents 3152b3d + 3072a61
commit c3a5da6
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/serlib/ser_uGraph.ml b/serlib/ser_uGraph.ml
@@ -41,6 +41,10 @@ let path_explanation_of_sexp = Serlib_base.opaque_of_sexp ~typ:"UGraph.path_expl
 type explanation = [%import: UGraph.explanation]
   [@@deriving sexp]
 
+type univ_variable_printers =
+  [%import: UGraph.univ_variable_printers]
+  [@@deriving sexp]
+
 type univ_inconsistency =
   [%import: UGraph.univ_inconsistency]
   [@@deriving sexp]
diff --git a/vendor/coq b/vendor/coq
+3 −12		.gitlab-ci.yml
+1 −3		Makefile.ci
+5 −0		dev/ci/ci-coq_lsp.sh
+3 −0		dev/ci/ci-serapi.sh
+0 −12		dev/ci/ci-serapi_test.sh
+1 −1		dev/doc/critical-bugs.md
+11 −6		dev/doc/xml-protocol.md
+7 −0		doc/changelog/02-specification-language/18929-master+program-equality-wrapper-multiple-inductive-families.rst
+0 −6		doc/changelog/02-specification-language/19088-master+fix19082-branch-length-mismatch.rst
+0 −5		doc/changelog/04-tactics/18944-prepare-proof-given-up.rst
+6 −0		doc/changelog/10-coqide/19040-master+fix-xmlprotocol-loc-line_nb-fail.rst
+74 −0		doc/sphinx/changes.rst
+154 −14		engine/evd.ml
+3 −0		engine/evd.mli
+47 −41		engine/uState.ml
+9 −9		engine/univSubst.ml
+3 −4		ide/coqide/coqOps.ml
+2 −2		ide/coqide/coqide.ml
+2 −5		ide/coqide/idetop.ml
+13 −0		ide/coqide/ideutils.ml
+1 −0		ide/coqide/ideutils.mli
+1 −1		ide/coqide/protocol/interface.mli
+13 −1		ide/coqide/protocol/serialize.ml
+11 −18		ide/coqide/protocol/xmlprotocol.ml
+12 −4		interp/constrintern.ml
+1 −1		interp/constrintern.mli
+9 −4		kernel/uGraph.ml
+2 −1		kernel/uGraph.mli
+134 −65		pretyping/cases.ml
+48 −11		pretyping/evarconv.ml
+19 −3		pretyping/evarconv.mli
+27 −14		pretyping/pretyping.ml
+42 −0		test-suite/bugs/bug_19054.v
+15 −0		test-suite/bugs/bug_1956.v
+29 −0		test-suite/bugs/bug_5777.v
+3 −0		test-suite/output/UnivBinders.out
+8 −0		test-suite/output/UnivBinders.v
+33 −0		test-suite/success/ProgramCases.v