aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Collapse)Author
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
vernac Reviewed-by: maximedenes
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based ↵Hugo Herbelin
generalization + cleanups Reviewed-by: herbelin
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged.
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
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
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 ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
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
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-04-02Add overlaysPierre Roux
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2019-03-31Add overlayPierre Roux
2019-03-31Merge PR #9733: [lexer] keyword protected quotation token for arbitrary textPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-03-31overlay for ltac2Enrico Tassi
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
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
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
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
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
Ack-by: gares Ack-by: herbelin Ack-by: mattam82 Ack-by: ppedrot
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker.
2019-02-28Overlays for coq/coq#9389 implicits API cleanupGaëtan Gilbert
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
Supersedes #8718.
2019-02-22overlay for EquationsEnrico Tassi
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
I think the usage looks cleaner this way.
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary.
2019-02-08Update overlay fileMatthieu Sozeau
2019-02-08Add overlay for EquationsMatthieu Sozeau
2019-02-08Add overlays for unicoq and mtac2Matthieu Sozeau
2019-02-05OverlaysMaxime Dénès
2019-02-04Overlays.Maxime Dénès
2019-01-24Add OverlaysMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 23:25:32 +0000