aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-13Merge section on Inductive types from Gallina and CIC.Théo Zimmermann
2020-05-13Create new file on Inductive types.Théo Zimmermann
2020-05-13Extract Inductive types from CIC.Théo Zimmermann
2020-05-13Merge sections on Inductive types and Recursive functions in new file.Théo Zimmermann
2020-05-13Add Recursive functions to new file on Inductive types.Théo Zimmermann
2020-05-13Extract Recursive functions from Gallina.Théo Zimmermann
2020-05-13Create new file on Inductive types.Théo Zimmermann
2020-05-13Extract Inductive types from Gallina.Théo Zimmermann
2020-05-13Merge PR #12293: Fix timestamp of coqchk manpageThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-12Merge PR #12309: Remove documentation of -compile, which was removed in #8690.Clément Pit-Claudel
2020-05-13Merge PR #12307: Cleaning up the legacy proof engineEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: kyoDralliam
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-12Remove documentation of -compile, which was removed in #8690.Théo Zimmermann
2020-05-12Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.leAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables ↵Pierre-Marie Pédrot
indirectly dependent in goal Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-12Merge PR #12190: [stdlib] [Permutation] Declare more instances as GlobalAnton Trunov
Reviewed-by: JasonGross Reviewed-by: anton-trunov
2020-05-12Remove a unused legacy tactic from Clenv.Pierre-Marie Pédrot
2020-05-12Write the outermost part of the legacy refiner directly in the monad.Pierre-Marie Pédrot
2020-05-12Clean up the legacy refiner implementation.Pierre-Marie Pédrot
We avoid using global-access primitives and instead rely on purely functional passing of the relevant data. Namely, we replace the goal argument with its environment, and we pass the additional check parameter.
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
They were not used anywhere anymore.
2020-05-12Remove useless try-with clauses in newring.Pierre-Marie Pédrot
This is already protected by then enter block.
2020-05-12Wrap the legacy refiner type into the Logic API.Pierre-Marie Pédrot
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
This was useless, since we did not observe the difference on evars.
2020-05-12documenting with examples the dynamic behaviour of Ltac2 SetKenji Maillard
2020-05-12Remove useless try-with blocks in congruence.Pierre-Marie Pédrot
The inner body was not raising any exception since it was in the monad, and even if it did so, the enter block would have caught it.
2020-05-12Merge PR #12303: [changelog] Fuse changelogs for #11249 and #12237Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-12fuse changelogs for #11249 and #12237Olivier Laurent
2020-05-11More tests of rebinding Ltac2 definitionsKenji Maillard
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo Herbelin
Reviewed-by: herbelin
2020-05-11Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlibHugo Herbelin
Reviewed-by: JasonGross
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-11Correcting ltac2's documentation on values turning test into proper check.Kenji Maillard
2020-05-11Generalize the Ltac2 value criterion to pure let-bindings.Pierre-Marie Pédrot
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-05-11Merge PR #12129: Add a `with_strategy` tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: herbelin Ack-by: ppedrot
2020-05-10Remove (outdated) timestamps from man pagesKartik Singhal
2020-05-10Merge PR #12235: Ensure eintros allows creating evarsKenji Maillard
Reviewed-by: kyoDralliam
2020-05-10Merge PR #12287: Define CRzero and CRone via CR_of_QMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-10Change log for #12223.Hugo Herbelin
2020-05-10Adding tests for error locationHugo Herbelin
2020-05-10Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255).Hugo Herbelin
Since we don't always have the call trace anymore, we explicitly insert a catch of failures in TacAlias. The trace is then treated in this catch rather than propagated to the underlying calls (a VFun?). I hope this is doing the same. The suggestion to use a tclOR is from P.-M. Pédrot. Note: this is not fully ideal, the messages which were expecting a trace should be rethought to take into account either that the calls are not printed anymore, or to print them again.
2020-05-10Merge PR #12286: [sphinx] Add links to other versions of the refmanThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-05-09Merge PR #12241: [declare] Merge DeclareDef into DeclareGaëtan Gilbert
Reviewed-by: Matafou Reviewed-by: SkySkimmer
2020-05-09Add another note about removing a tactic after abstractJason Gross
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18. We instead add a warning in the manual and a kludge in the test-suite.
2020-05-09[with_strategy] Fix for coqchkJason Gross
We need to record the transparency information in the libobject stack in order for coqchk to not trip over the strategy information. This is quite sketchy, though.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:55:50 +0000