aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-28Generalize type of compare_head_with functionsGaëtan Gilbert
2018-09-28Merge PR #8578: [dune] Allow to build CI after a Dune build.Gaëtan Gilbert
2018-09-28Merge PR #8479: Fix #8478: Undeclared universe anomaly with sectionsPierre-Marie Pédrot
2018-09-28Merge PR #8509: Fix numerous anomalies with Scheme EqualityPierre-Marie Pédrot
2018-09-28Merge PR #8576: [api] Remove unnecessary type alias introduced in 8.9Pierre-Marie Pédrot
2018-09-28Merge PR #8569: [dune] [configure] Further tweaks for interactive use.Théo Zimmermann
2018-09-28Merge PR #8568: [dune] [coqide] Turn CoqIDE into a library.Théo Zimmermann
2018-09-27Merge PR #8545: Functionalize evarmap passing in Cases.mlEmilio Jesus Gallego Arias
2018-09-27Merge PR #8570: [ssr] [camlp5] Remove warning from camlp5Enrico Tassi
2018-09-27[configure] [dune] Don't force the Dune user to set envars.Emilio Jesus Gallego Arias
In order to support sending the OPAM prefix to configure via Dune, we introduced a `COQ_CONFIGURE_PREFIX` variable. However, this had the pitfall that now the developer had to set it or else face a hanging build due to configure expecting user input. While we wait for a larger cleanup in `-prefix`, we introduce a `no-ask` option in `./configure` that will avoid this problem. If `-no-ask` is passed to `configure` no interactive question or display will be shown to the user.
2018-09-27[configure] Don't die if the build sandbox doesn't have the stdlib.Emilio Jesus Gallego Arias
Dune calls `./configure` under the build sandbox, which, if the voboot target has not been executed will contain only the OCaml parts of Coq. Thus, we make configure not to die if the `plugins` directory is not present. This makes Dune usable without calling the `voboot` target.
2018-09-27[ci] Allow `make ci-$contrib` when we have a build under Dune.Emilio Jesus Gallego Arias
This should allow people to test CI contribs under Dune. It should be good for now but it is still a work in progress.
2018-09-27[coqc] Use standard binary location routine from libEmilio Jesus Gallego Arias
Instead of rolling our own, we use the standard one that works well when binaries are symlinked.
2018-09-27[api] Remove unnecessary type alias introduced in 8.9Emilio Jesus Gallego Arias
This was introduced in #7820 and it is not needed indeed. As 8.9 was not released we don't need to perform a deprecation phase.
2018-09-27Merge PR #6524: [print] Restrict use of "debug" Termops printer.Pierre-Marie Pédrot
2018-09-27Merge PR #8559: [api] Two more missing deprecations.Pierre-Marie Pédrot
2018-09-27Using Constant.change_label (better level of abstraction to build kernel names).Hugo Herbelin
2018-09-27Scheme Equality: support for working in a context of Parameters.Hugo Herbelin
It was working in very specific context of section variables. We make it work similarly in the same kind of specific context of Parameters. See test file SchemeEquality.v for the expected form. See discussion at PR #8509.
2018-09-27Fixing a Scheme Equality anomaly with constants bound to inductive.Hugo Herbelin
2018-09-27Fixing a typo in a comment.Hugo Herbelin
2018-09-27Fixing #4859 (anomaly with Scheme called on inductive type with indices).Hugo Herbelin
We raise a normal error instead of an anomaly.
2018-09-27Fixing #4612 (anomaly with Scheme called on unsupported inductive type).Hugo Herbelin
We raise a normal error instead of an anomaly. This fixes also #2550, #8492. Note in passing: While the case of a type "Inductive I := list I -> I" is difficult, the case of a "Inductive I := list nat -> I" should be easily doable.
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
Instead of looking into the name-oriented structure we look into the actual section structures. Note: together with #8475 this lets us remove UnivNames.add_global_universe.
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-27Merge PR #8562: [build] Re-enable warning 59.Gaëtan Gilbert
2018-09-27Merge PR #8571: [stdlib] Fix warning due to missing Declare Scope in BvectorHugo Herbelin
2018-09-27[stdlib] Fix warning due to missing Declare Scope in BvectorEmilio Jesus Gallego Arias
This broke the build so it should be merged quickly.
2018-09-27[ssr] [camlp5] Remove warning from camlp5Emilio Jesus Gallego Arias
Current compilation of ssrparser.ml4 produces: ``` coqp5 plugins/ssr/ssrparser.ml Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex]. ``` the solution is easy.
2018-09-27[dune] [coqide] Turn CoqIDE into a library.Emilio Jesus Gallego Arias
As noted by @anton-trunov, this is more useful for development and debug.
2018-09-26Merge PR #8171: Bvector: add BVeq and some notationsHugo Herbelin
2018-09-26[build] Re-enable warning 59.Emilio Jesus Gallego Arias
After #8043 was fixed we can come back to a stricter warning profile for flambda.
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
The functions in `Termops.print_*` are meant to be debug printers, however, they are sometimes used in non-debug code due to a API confusion. We thus wrap such functions into an `Internal` module, improve documentation, and switch users to the right API.
2018-09-26Merge PR #8561: Fix votour compilation after #8102.Emilio Jesus Gallego Arias
2018-09-26Fix votour compilation after #8102.Pierre-Marie Pédrot
2018-09-26Merge PR #8102: Fix #8043: Unsafe assignment in checker.Maxime Dénès
2018-09-26Merge PR #8497: Use "rm -rf" in "make clean" so .coq-native directories are ↵Maxime Dénès
removed
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
2018-09-26Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)Maxime Dénès
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-26Merge PR #7571: [kernel] Compile with almost all warnings enabled.Maxime Dénès
2018-09-26Merge PR #7309: Made names of existential variables interpretable as Ltac ↵Pierre-Marie Pédrot
variables.
2018-09-26Making cases.ml use state-passing instead of the evdref idiom.Pierre-Marie Pédrot
2018-09-26Merge PR #8419: Remove romega in favor of liaThéo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-26Merge PR #8217: Fixes #8215: "critical" type inference bug in interpreting ↵Pierre-Marie Pédrot
evars by name
2018-09-26[api] Two more missing deprecations.Emilio Jesus Gallego Arias
We missed two more constructor / record deprecation.
2018-09-25Merge PR #8535: Fixing #8532: regression in Print Assumptions within a functor.Pierre-Marie Pédrot
2018-09-25Merge PR #8552: [ci] [docker] elpi version 1.1.0Emilio Jesus Gallego Arias
2018-09-25Merge PR #8549: Fix issues introduced by the PDF manual mergeThéo Zimmermann
2018-09-25overlay to test elpi 1.1Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:24:45 +0000