aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-14Tweak the error message of reference internalization.Pierre-Marie Pédrot
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.Gaëtan Gilbert
2020-05-14Merge PR #12320: [ci] [sf] Fix SF build.Gaëtan Gilbert
2020-05-14Merge PR #12214: nit: don't open Persistent_cache in micromegaVincent Laporte
2020-05-14[ci] [sf] Fix SF build.Emilio Jesus Gallego Arias
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
2020-05-14Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.Emilio Jesus Gallego Arias
2020-05-14Merge PR #12244: Store the OCaml version used for Coq in vo files.Emilio Jesus Gallego Arias
2020-05-13Adding change log for #8808.Hugo Herbelin
2020-05-13Overlay elpiHugo Herbelin
2020-05-13Documenting notations with both terms and binders.Hugo Herbelin
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-13Merge PR #12293: Fix timestamp of coqchk manpageThéo Zimmermann
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:57:46 +0000