aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Expand)Author
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
2019-06-12Merge PR #10358: [docker] update elpi to 1.3.1Gaëtan Gilbert
2019-06-11overlayEnrico Tassi
2019-06-11Adding an overlay for Equations.Pierre-Marie Pédrot
2019-06-11Overlays for 10319Gaëtan Gilbert
2019-06-09[ci] Overlays for move_termination_routine_outEmilio Jesus Gallego Arias
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-06Remove old overlaysGaëtan Gilbert
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-04update overlaysEnrico Tassi
2019-06-04Overlays for coq/coq#10050 (proof_global API changes)Gaëtan Gilbert
2019-06-01Adding overlay for elpiHugo Herbelin
2019-05-27Overlay for mind_kelim change (#10133)Gaëtan Gilbert
2019-05-24Adding overlays.Pierre-Marie Pédrot
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Overlay for removing Instance: !type syntaxGaëtan Gilbert
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-13Add overlay for UnicoqMaxime Dénès
2019-05-10Add overlay for elpiVincent Laporte
2019-05-10Add overlays for coq/coq#10052.Pierre-Marie Pédrot
2019-05-07Add overlays.Pierre-Marie Pédrot
2019-04-20overlay for elpiEnrico Tassi
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-10Overlays for Global removal in pretyperMaxime Dénès
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Add overlaysPierre Roux
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
2019-03-31Add overlayPierre Roux
2019-03-31Merge PR #9733: [lexer] keyword protected quotation token for arbitrary textPierre-Marie Pédrot
2019-03-31overlay for ltac2Enrico Tassi
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-30Overlay for ElpiVincent Laporte
2019-03-27[proof_global] [ci] Overlays for removal of imperative state.Emilio Jesus Gallego Arias
2019-03-26Overlays for HoTT, Ltac2, and UniMathVincent Laporte
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...Maxime Dénès
2019-03-20Add overlays for printer API changesMaxime Dénès
2019-03-14Overlays for SPropGaëtan Gilbert
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi