aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-16Warning on hint commands that have no explicit locality.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
Reviewed-by: anton-trunov Reviewed-by: Blaisorblade
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ↵coqbot-app[bot]
sort elimination constraints Reviewed-by: gares
2020-11-15Merge PR #12611: [record] Cleanup of data structure and functionscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares
2020-11-15Merge PR #13374: [dune] [opam] Generate opam files automatically using Dune.coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block ↵Li-yao Xia
verbatim from inline verbatim Reviewed-by: Lysxia
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an ↵coqbot-app[bot]
error, not an anomaly Reviewed-by: ejgallego
2020-11-15[dune] [opam] Generate opam files automatically using Dune.Emilio Jesus Gallego Arias
- closes #12376 : dune version is now consistent as suggested - cc #12858 : coqide and coqide-server do no depend on ocamlfind when built this way. - closes #13372 : more precision in the license identifier
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a ↵coqbot-app[bot]
handler in NotFoundInstance Reviewed-by: ejgallego
2020-11-15Merge PR #13368: Fix dune rules for @check-gram following recent changes.coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-15Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve ↵coqbot-app[bot]
description of Instance command Reviewed-by: Zimmi48
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
2020-11-15Adding an output test to check that the hint commands respect their locality.Pierre-Marie Pédrot
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-15Add changelog for #13383.Hugo Herbelin
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not ↵Pierre-Marie Pédrot
a keyword. Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-15Merge PR #13356: Make the universe of primitive arrays irrelevantPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-14Coqdoc: we move a newline at a better place.Hugo Herbelin
This does not affect the rendering but gives better structured html/tex files.
2020-11-14Documenting one-line verbatim.Hugo Herbelin
2020-11-14Addressing #13304: how to verbatim an expression mentioning >>.Hugo Herbelin
We clarify that there are two kinds of verbatim: inline and block. We add a test testing verbatim and others. Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-11-14Merge PR #13369: Move destructuring let syntax closer to its documentation.coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Dead code in coqdoc.Hugo Herbelin
2020-11-14Reorganizing the printing of warnings; fixing line count.Hugo Herbelin
The line count remains fragile though... Any idea to do it automatically?
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
Fixes #13266 (see #12675, 8641cb7385).
2020-11-13[record] Some documentation + minor refactoringEmilio Jesus Gallego Arias
Co-authored-by: <Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
Fix #13348
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
Fix #13354 This change is very specific to array, but should not be a significant obstacle to generalization of the feature to eg axioms if we want to later.
2020-11-13Remove unused CClosure.FNativeEntries.farrayGaëtan Gilbert
BTW it was incorrect (array needs an instance)
2020-11-13Fix dune rules for @check-gram following recent changes.Théo Zimmermann
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
Reviewed-by: Blaisorblade Ack-by: SkySkimmer
2020-11-13Add changelog for #13365Li-yao Xia
2020-11-13Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freeLi-yao Xia
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-12Add changelog entry for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Test case for Proof using in -noinit mode.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:03:28 +0000