aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-11-11We move the example of Makefile wrapper next to the explanations about ↵Hugo Herbelin
CoqMakefile. Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
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
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause ↵Pierre-Marie Pédrot
of a match. Reviewed-by: ppedrot
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
Reviewed-by: anton-trunov
2020-11-08fixupCyril Cohen
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-06Update doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rstCyril Cohen
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 13:55:23 +0000