aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-11Merge PR #9551: Small typos in the documentation.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-11Merge PR #9540: [ssr] keep user annotation on views (fix #9538)Cyril Cohen
Reviewed-by: CohenCyril Fixes a bug introduced by PR #9341
2019-02-11Merge PR #9544: [coqargs] Minor refactoring of error functions.Enrico Tassi
Reviewed-by: gares
2019-02-11Merge PR #9531: [test-suite] Improve test for async workers.Enrico Tassi
Reviewed-by: gares
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-11Merge PR #9465: [Nix-CI] Add iris and lambda-rustMaxime Dénès
Reviewed-by: maximedenes
2019-02-11[coqargs] Minor refactoring of error functions.Emilio Jesus Gallego Arias
We remove a few ad-hoc `exit` from the code as error handling really ought to be centralized.
2019-02-11Merge PR #9541: [stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-11Merge PR #9543: [ocamldebug] Fix load order after gramlib refactoring.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-11Merge PR #9522: Update link to refman for master branch.Vincent Laporte
Reviewed-by: vbgl
2019-02-11[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Enrico Tassi
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-02-11[ocamldebug] Fix load order after gramlib refactoring.Emilio Jesus Gallego Arias
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-08[test-suite] Improve test for async workers.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 02:45:19 +0000