aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-02-07[dune] Fix OCaml trunk build.Emilio Jesus Gallego Arias
I forgot to change the profile call; we should find some better solution but that's OK for now.
2019-02-06[Gitlab-CI] Deploy manual to GH-PagesVincent Laporte
2019-02-06Avoid eqn when generating name in induction_gen.Jasper Hugunin
Fixes #9494. Was failing with "Cannot create self-referring hypothesis" when the generated name equaled the eqn.
2019-02-06Merge PR #9124: Document the possibility of declaring a Ltac name_goal.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-02-06Merge PR #9456: The lowest universe level is 1.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-06Makefiles: Fixes for byte compilationGaëtan Gilbert
- default targets don't depend on ocamlopt when it's unavailable - coqc.byte is built by byte target and coqc by coqbinaries target - unit tests use best ocaml - poly-capture-global-univs tests ml compilation with ocamlc - don't try to install .cmx and native-compute .o files cf https://github.com/coq/coq/issues/9464
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:25:49 +0000