aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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
2018-09-24[ci] [docker] Move to OPAM 2.0Emilio Jesus Gallego Arias
The OPAM 1.2 repository has been frozen, thus we must use OPAM 2.0 if we want to get newer versions of packages / compilers. For now we must perform a manual install of OPAM as no packages for Ubuntu 18.04 exist. Note that this means nothing about the installability of Coq itself, whose OPAM repository should remain in 1.2 format for quite a long period.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:44:32 +0000