aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-13Create new file on sorts.Théo Zimmermann
2020-05-13Extract Sorts out of CIC.Théo Zimmermann
2020-05-13Merge PR #12293: Fix timestamp of coqchk manpageThéo Zimmermann
2020-05-13Added change log.Hugo Herbelin
2020-05-13Ssrmatching: Hack to circumvent a hack.Hugo Herbelin
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-05-13do not re-export ListNotations from Program: kill overlaysAntonio Nikishaev
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-13Centralize the OCaml version-checking function.Pierre-Marie Pédrot
2020-05-13Store the OCaml version used for Coq in vo files.Pierre-Marie Pédrot
2020-05-13Test interleaving of command-line options.Théo Zimmermann
2020-05-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-13Clarify the assignee's role in removing the overlay informationAnton Trunov
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
2020-05-13Clarify the documentation for merging PRs with overlaysAnton Trunov
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 01:54:54 +0000