aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-12Fix failing coqtops in syntax-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coqide.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coq-library.rstGaëtan Gilbert
Mostly in the pattern ~~~ .. coqtop:: in Theorem foo : bla. Theorem bar : blah. (* nested proof error *) ~~~
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-12Fix undefined SPHINX_DEPS when QUICKGaëtan Gilbert
2019-02-12Fix doc for coqtop:: undoGaëtan Gilbert
2019-02-12Increase sphinx recursion limitGaëtan Gilbert
Not sure why but it seems required for future commits.
2019-02-11Merge PR #9522: Update link to refman for master branch.Vincent Laporte
Reviewed-by: vbgl
2019-02-11Merge PR #9478: Remove the comment fields of locations.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-11Merge PR #9534: Workaround for CI not having enough RAM for bedrock2: ↵Emilio Jesus Gallego Arias
`-async-proofs-tac-j 1` Reviewed-by: ejgallego
2019-02-10Merge PR #9535: [readme] Add link to information about release plans.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-02-10Merge PR #9536: [ci] Remove unused bintray file.Maxime Dénès
Reviewed-by: maximedenes
2019-02-09remove `allow_failure: true` for bedrock2Samuel Gruetter
2019-02-09remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed ↵Samuel Gruetter
passed https://gitlab.com/coq/coq/-/jobs/158737429
2019-02-09Update link to refman and stdlib doc for master branch.Théo Zimmermann
2019-02-09[ci] Remove unused bintray file.Emilio Jesus Gallego Arias
Not needed anymore after Travis was removed.
2019-02-09[readme] Add link to information about release plans.Emilio Jesus Gallego Arias
This is a proposal to use the wiki to gather current information about the release process.
2019-02-08Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`Samuel Gruetter
COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile, and we use VERBOSE=1 for better debuggability
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
Reviewed-by: gares
2019-02-08Merge PR #9492: [stm] Filter some more arguments that shouldn't be sent to ↵Enrico Tassi
workers. Reviewed-by: gares
2019-02-08Merge PR #9504: Add print_pure_econstr signatureGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-08Merge PR #9513: Edit release-process.md to ease upcoming releases of Coq in ↵Théo Zimmermann
Docker Hub Reviewed-by: Zimmi48
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
This fixes #9484 .
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
Ack-by: SkySkimmer Reviewed-by: aspiwack Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: mattam82 Ack-by: maximedenes
2019-02-08Merge PR #9515: [Gitlab-CI] Automatic deployment of the standard library ↵Emilio Jesus Gallego Arias
documentation to GH-pages Reviewed-by: ejgallego
2019-02-08[Gitlab-CI] Automatic deployment of the standard library documentation to ↵Vincent Laporte
GH-pages
2019-02-08Add item in release-process.md to ease upcoming releases of Coq in Docker HubErik Martin-Dorel
Related: coq/bignums#17 [ci skip]
2019-02-07Merge PR #9499: [Gitlab-CI] Never attempt to build cachixThéo Zimmermann
Reviewed-by: Zimmi48
2019-02-07Merge PR #9477: Makefiles: Fixes for byte compilationEnrico Tassi
Reviewed-by: gares
2019-02-07Merge PR #9475: Automatic deployment of the user manual to GH-PagesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: vbgl
2019-02-07Add print_pure_econstr signatureThierry Martinez
print_pure_econstr was not exported (while print_pure_constr was).
2019-02-07[Gitlab-CI] Never attempt to build cachixVincent Laporte
2019-02-07Merge PR #9496: Avoid eqn when generating name in induction_gen.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-07Merge PR #9498: [dune] Fix OCaml trunk build.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-07Merge PR #9479: Remove the Plexing.Error exception.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:20:55 +0000