aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-09Merge PR #12204: Ltac helper functions APIHugo Herbelin
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-09Merge PR #12040: Document the signing procedure of released binary packages.Maxime Dénès
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
2020-05-08Merge PR #12272: Cleanup formatting in .. coqtop:: directivesClément Pit-Claudel
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
2020-05-08Merge PR #12268: Add an example to motivate strictly positive occurrences checkThéo Zimmermann
2020-05-08Merge PR #12068: Coqide completion: tentative fix for #11943Pierre-Marie Pédrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.Gaëtan Gilbert
2020-05-07Merge PR #12262: Fix #12211 (TIMED for ocaml files doesn't print file name)Gaëtan Gilbert
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-07Merge PR #12267: [ci] bump elpi to 1.11Emilio Jesus Gallego Arias
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-07[ci] overlay for coq-elpiEnrico Tassi
2020-05-07Export API to recover values out of Ltac application.Pierre-Marie Pédrot
2020-05-07Add helper API to define low-level Ltac functions.Pierre-Marie Pédrot
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-06Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and m...Hugo Herbelin
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
2020-05-06Merge PR #12018: Adding properties about implb in Bool.vAnton Trunov
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-06Fix #12211Jason Gross
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
2020-05-05Merge PR #12252: [refman] Add missing (only parsing) to example of compat not...Clément Pit-Claudel
2020-05-05Fix GeoCoq slowdown.Pierre-Marie Pédrot
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
2020-05-04update documentation for overlay buildingOlivier Laurent
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 15:21:03 +0000