aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-13Merge PR #12307: Cleaning up the legacy proof engineEmilio Jesus Gallego Arias
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
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
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-12Merge PR #12190: [stdlib] [Permutation] Declare more instances as GlobalAnton 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
2020-05-12Interleave commandline require/set/unset commandsLasse Blaauwbroek
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
2020-05-12Remove useless try-with clauses in newring.Pierre-Marie Pédrot
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
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
2020-05-12Merge PR #12303: [changelog] Fuse changelogs for #11249 and #12237Théo Zimmermann
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
2020-05-11Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlibHugo Herbelin
2020-05-11Checking validity of coqdoc file name.Hugo Herbelin
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
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
2020-05-10Remove (outdated) timestamps from man pagesKartik Singhal
2020-05-10Add overlays.Pierre-Marie Pédrot
2020-05-10Further cleanup: remove the local_reduction_function type.Pierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-10Merge PR #12235: Ensure eintros allows creating evarsKenji Maillard
2020-05-10Merge PR #12287: Define CRzero and CRone via CR_of_QMichael Soegtrop
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
2020-05-10Merge PR #12286: [sphinx] Add links to other versions of the refmanThéo Zimmermann
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
2020-05-09Add another note about removing a tactic after abstractJason Gross
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
2020-05-09[with_strategy] Fix for coqchkJason Gross
2020-05-09Fix a bug with with_strategy, behavior on multisuccess tacticsJason Gross
2020-05-09[with_strategy] Work around #12191Jason Gross
2020-05-09Work around a bug in Coq in the docJason Gross
2020-05-09Elaborate with_strategy warningJason Gross
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Add overlaysPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 04:04:35 +0000