aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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 #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-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
2019-02-06Merge PR #9487: Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Enrico Tassi
Ack-by: Zimmi48 Reviewed-by: gares
2019-02-06Fix #9486: Makefile.install should not have a target fooGaëtan Gilbert
2019-02-06Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Théo Zimmermann
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
Before #9263 this type was returned by the STM's `parse_sentence`, but the type was lost on the generalization to entries.
2019-02-05Merge PR #9397: Simplify code for Recordops.cs_pattern_of_constrMatthieu Sozeau
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: mattam82
2019-02-05Merge PR #9472: Add advice and an example to the documentation of fold.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-02-05Remove the Plexing.Error exception.Pierre-Marie Pédrot
This was dead code, it was never raised ever.
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive ↵Pierre-Marie Pédrot
records Reviewed-by: ppedrot
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-02-05Merge PR #9396: Skip indirection through Evd for obligation ustate manipulationMatthieu Sozeau
Reviewed-by: mattam82
2019-02-05Merge PR #8421: [dune] Fix Dune build in Windows.Théo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-02-05OverlaysMaxime Dénès
2019-02-05Make Program a regular attributeMaxime Dénès
We remove all calls to `Flags.is_program_mode` except one (to compute the default value of the attribute). Everything else is passed explicitely, and we remove the special logic in the interpretation loop to set/unset the flag. This is especially important since the value of the flag has an impact on proof modes, so on the separation of parsing and execution phases.
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-02-04Merge PR #9470: the default branch of Mtac2 changed to masterEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-04Merge PR #9468: Remove AppVeyor: superseded by Azure.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-02-04the default branch of Mtac2 changed to masterbeta
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
In order for Dune to work in Windows we need to tweak some script calls, they need a POSIX shell and the `(run ...)` / `(system ...)` actions use `cmd.exe` on Windows. Hopefully, we will rely less on `bash` when Dune can understand Coq libraries. This affects shell scripts in `kernel/**.sh` for example. It is interesting to see how faster the Coq Windows build is with Dune + Windows. There are some problems with PATHs that prevent the test suite from working, these will be fixed in a future PR.
2019-02-04Remove AppVeyor: superseded by Azure.Théo Zimmermann
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-02-04Merge PR #9144: Fixes #4633: clearer message unknown existentialPierre-Marie Pédrot
Ack-by: herbelin Reviewed-by: ppedrot
2019-02-04Merge PR #9409: Move non-primitive-record warning to ↵Pierre-Marie Pédrot
declare_mutual_inductive_with_eliminations Reviewed-by: ppedrot
2019-02-04Merge PR #9437: Comment universe operations in Classes.contextPierre-Marie Pédrot
Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:56:06 +0000