aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
E.g. Locate "(x , y , .. , z )" now works while only Locate "(_ , _ , .. , _ )" was working before. This also fixes a confusion between a variable and its anonymization into _, wrongly finding notations mentioning '_'. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
This is a better abstraction barrier (no "symbol" type with uninterpreted ".." exported out of notation.ml). It also allows to "browse" notations mentioning a "..".
2020-11-15Indentation.Hugo Herbelin
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-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-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-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-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-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-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
2020-11-12Revert to "using" not being a keyword in -noinit mode.Théo Zimmermann
The IDENT annotations in g_ltac.mlg are required to not break the parser.
2020-11-12Add support for Proof using in -noinit mode.Théo Zimmermann
"Proof with" is Ltac-specific but there is no reason why it should be the same for "Proof using".
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:21:26 +0000