aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-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
2018-09-25elpi 1.1.0Enrico Tassi
2018-09-25Merge PR #8235: NArith: deprecate N2Bv_genHugo Herbelin
2018-09-25Fixing #8532 (regression in Print Assumptions within a functor).Hugo Herbelin
The regression was introduced in 1522b989 (PR #7193) which itself was fixing bug #7192. (Note another regression of the same commit which is fixed in #8416.)
2018-09-25Fix Sphinx manual targets.Théo Zimmermann
New targets refman, refman-html and refman-pdf. sphinx keeps its previous meaning (compatibility alias for refman-html). install-doc-sphinx has been accidentally renamed.
2018-09-25Fix title of Introduction chapter in HTML version.Théo Zimmermann
And location of footnote.
2018-09-25[doc] Rename credits-wrapper to credits and credits to credits-contentsClément Pit-Claudel
This ensures that previous links to 'credits.html' still point to the right page.
2018-09-25[doc] Change Sphinx project title back to "Coq"Clément Pit-Claudel
Use 'The Coq Reference Manual' only in LaTeX.
2018-09-25[doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJaxClément Pit-Claudel
2018-09-25Remove romegaVincent Laporte
2018-09-25Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al.Pierre-Marie Pédrot
2018-09-25Merge PR #8550: Don't use dune-template for apidocEmilio Jesus Gallego Arias
2018-09-24Don't use dune-template for apidocGaëtan Gilbert
dune-template works for the build jobs but followup jobs are different enough to make reuse more confusing than useful IMO.
2018-09-24Fixes #8215 ("critical" bug of type inference in interpreting evars by names).Hugo Herbelin
When interpreting an existential variable "?n@{inst}" in the current context, check that variables bound to local definitions are replaced by variables with convertible body. Also give a message explaining the type error or non-convertibility error rather than wrongly saying that there is no binding for the variable.
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
This is a partial resurrection of #6423 but only for the kernel. IMHO, we pay a bit of price for this but it is a good safety measure. Only warning "4: fragile pattern matching" and "44: open hides a type" are disabled. We would like to enable 44 for sure once we do some alias cleanup.
2018-09-24Merge PR #8541: Update flag, option and table descriptions in coqdomain.py, ↵Clément Pit-Claudel
update README.rst to match.
2018-09-24Merge PR #8520: [ci] [docker] Move to OPAM 2.0Gaëtan Gilbert
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
After the introduction of `EConstr`, "normalization" has become unnecessary, we thus deprecate the `nf_*` family of functions. Test-suite and CI pass after the fix for #8513.
2018-09-24Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.Pierre-Marie Pédrot
2018-09-24Merge PR #8527: dev/doc/profiling.txt: per-component flame graphsPierre-Marie Pédrot
2018-09-24Merge PR #8464: Fix numeral notationsHugo Herbelin
2018-09-24Merge PR #8530: Fix typo in comment.Hugo Herbelin
2018-09-24Merge PR #8536: Fix #8513: EConstr.eq_constr doesn't properly take into ↵Gaëtan Gilbert
account universe variables
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:12:52 +0000