aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06Merge PR #12018: Adding properties about implb in Bool.vAnton Trunov
Ack-by: Blaisorblade Reviewed-by: anton-trunov
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
Reviewed-by: gares
2020-05-05Merge PR #12252: [refman] Add missing (only parsing) to example of compat ↵Clément Pit-Claudel
notations.
2020-05-05Fix GeoCoq slowdown.Pierre-Marie Pédrot
There is no point in normalizing the goal in the legacy refiner because the function is actually insensitive to evars.
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-05[ssr] wrap a couple of exception with tclLIFTEnrico Tassi
2020-05-04[ssr] get rid of (pf_)mkSsrConstEnrico Tassi
2020-05-04Merge PR #12225: [ci] [doc] More detailed documentation for overlay buildingThéo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-05-04update documentation for overlay buildingOlivier Laurent
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-04Merge PR #12220: [dune] [doc] TweaksGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-04[dune] [doc] TweaksEmilio Jesus Gallego Arias
Close #12167
2020-05-04add order properties about boolOlivier Laurent
2020-05-03Merge PR #12231: Simplify division of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-03Merge PR #12238: [stdlib] [CPermutation] patch for #12031Hugo Herbelin
Reviewed-by: herbelin
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-03Add tests uncovered during bug chasing in the CI.Pierre-Marie Pédrot
2020-05-03Add overlays.Pierre-Marie Pédrot
2020-05-03Further port of ssr tacticsPierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Remove legacy API in SSR.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tacticsPierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further SSR port.Pierre-Marie Pédrot
2020-05-03Remove legacy SSR API.Pierre-Marie Pédrot
2020-05-03Further SSR port.Pierre-Marie Pédrot
2020-05-03Remove legacy layer in SSR.Pierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR code.Pierre-Marie Pédrot
2020-05-03Export new combinators in SSR not relying on the legacy API.Pierre-Marie Pédrot
2020-05-03Further porting of ssrcode.Pierre-Marie Pédrot
2020-05-03Slightly more tricky port of the ssr tactics.Pierre-Marie Pédrot
2020-05-03Export missing tacticals.Pierre-Marie Pédrot
2020-05-03Further port SSReflect tactics to the new engine.Pierre-Marie Pédrot
2020-05-03Wrap ssr tactics into V82.tactic.Pierre-Marie Pédrot
Porting them is still to be done, but at least we don't rely on the wrapper everywhere.
2020-05-03Wrap a monadic combinator in a try-with block to catch exceptions.Pierre-Marie Pédrot
Moving code around uncovered this bug.
2020-05-03Remove a call to V82.tactic in Btauto.Pierre-Marie Pédrot
2020-05-03Remove a very specific low-level tactical from Refiner.Pierre-Marie Pédrot
It was only used at one point in the STM, and its localization was suprising to say the least. Furthermore it was relying on legacy code. Instead we hardcode it in the STM.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:08:49 +0000