aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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
2019-02-04Overlays.Maxime Dénès
2019-02-04Primitive integersMaxime Dénès
This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2019-02-04Dockerfile: update menhir from 20180530 to 20181113Vincent Laporte
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-02-04Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.Maxime Dénès
Reviewed-by: maximedenes Ack-by: ppedrot
2019-02-04Merge PR #9426: [test-suite] Fix display of check.Enrico Tassi
Reviewed-by: gares
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-02-04Merge PR #9461: Fix default goal selector error message.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
Reviewed-by: fajb
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
Ack-by: mattam82 Reviewed-by: ppedrot
2019-02-02Merge PR #9395: Global [open Univ] in UStatePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-01Fix default goal selector error message.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:36:26 +0000