aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-13[record] [ci] Overlay for elpiEmilio Jesus Gallego Arias
We re-expose `declare_projections` and `declare_structure_entry` as it is needed by coq-elpi. Ideally we would provide a better way in recordops to interact with this, in fact `declare_structure_entry` is just a wrapper around recordops + libobject structure so there is hope it goes away entirely in the future. The need for Elpi to manually call `declare_projections` should actually disappear in future refactorings.
2020-11-13[record] Options API cleanup.Emilio Jesus Gallego Arias
2020-11-13[record] Refactor nested functions.Emilio Jesus Gallego Arias
In preparation for better handling of the regular record / class codepath. This will also allow to pack record data better.
2020-11-13[record] Cleanup of data structure and functions [2/2]Emilio Jesus Gallego Arias
In preparation for reworking the record declaration path to use the common infrastructure, we perform some refactoring. The current choices are far from definitive, as we will consolidate the data types more as we move along with the work here.
2020-11-13[record] Cleanup of data structure and functions [1/2]Emilio Jesus Gallego Arias
In preparation for reworking the record declaration path to use the common infrastructure, we perform some refactoring. The current choices are far from definitive, as we will consolidate the data types more as we move along with the work here.
2020-11-13Merge PR #13358: Merge the Linked / LinkedInteractive native link ↵coqbot-app[bot]
information constructors Reviewed-by: SkySkimmer
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
Reviewed-by: Blaisorblade Ack-by: SkySkimmer
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-12Merge PR #13318: Turn ssr proxy notation for supporting ↵coqbot-app[bot]
second-order/contextual pattern abbreviations to only parsing Reviewed-by: gares
2020-11-12Merge PR #13361: Move last changelog entry for 8.12.1.coqbot-app[bot]
Reviewed-by: ejgallego
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Merge PR #13359: Print failed test suite logs in CIcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, ↵coqbot-app[bot]
not only on subidentifiers of an identifier Reviewed-by: Zimmi48
2020-11-12Merge PR #13355: Fix Iris CI scriptcoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: RalfJung Ack-by: Zimmi48
2020-11-12Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle Ack-by: jashug Ack-by: ejgallego
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
in addition to having them as artefacts
2020-11-12Merge the Linked and LinkedInteractive constructors.Pierre-Marie Pédrot
There was not any difference between those after the cleanup patches that come before.
2020-11-12Statically ensure that the native interactive flag is always set to true.Pierre-Marie Pédrot
It was a hidden invariant of the code.
2020-11-12Statically ensure that native update locations are of form Linked*.Pierre-Marie Pédrot
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ↵Pierre-Marie Pédrot
naming Ack-by: gares Reviewed-by: ppedrot
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48 Ack-by: ppedrot Ack-by: jfehrle
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
I left the other test as a v file since it might become relevant when the corresponding Qed bug is fixed.
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
Polymorphic side-effects generated in monomorphic mode would be counted towards trusted subcomponents. This would allow to make ill-typed terms pass as legitimate by mimicking the shape of the inlining of monomorphic side-effects in such a proof.
2020-11-12Fix Iris CI scriptGaëtan Gilbert
Also add nice error message when the grep produces an empty result
2020-11-12Add changelog for #13345.Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48
2020-11-11Add changelog for #13351.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13335: Fix running unit tests with dune compiled coqcoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-10Merge PR #13315: Convert logic chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
(for runs outside dune, ie "make -C test-suite unit-tests" rather than "dune build @runtest") Fix #13333
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-10Merge PR #13322: [obligation] Properly handle no obligations on `Next ↵coqbot-app[bot]
Obligation` Reviewed-by: SkySkimmer
2020-11-10Merge PR #13297: Remove the native symbol registering from the safe environment.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, ↵coqbot-app[bot]
OCaml and Gallina. Reviewed-by: jfehrle Reviewed-by: cpitclaudel
2020-11-09Merge PR #13327: Fix documentation of Ltac ::=coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
Fixes #13320 . Trivial programming error, actually this is handled better in a further refactoring branch not submitted due to the long time the whole rework took.
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
2020-11-09Fix indentation of todo in Ltac chapter.Théo Zimmermann
Actual documentation was interpreted as a comment.
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
Instead we store that data in the native code that was generated in adapt the compilation scheme accordingly. Less indirections and less imperative tinkering makes the code safer. The global symbol table was originally introduced in #10359 as a way not to depend on the Global module in the generated code. By storing all the native-related information in the cmxs file itself, this PR also makes other changes easier, such as e.g. #13287.
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-09Merge PR #13310: Fix macOS CI on Azure.coqbot-app[bot]
Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 07:18:19 +0000