index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
dev
/
ci
/
user-overlays
Age
Commit message (
Expand
)
Author
2019-02-28
Constructor type information uses the expanded form.
Pierre-Marie Pédrot
2019-02-28
Overlays for coq/coq#9389 implicits API cleanup
Gaëtan Gilbert
2019-02-23
[vernac] Unify declaration hooks.
Emilio Jesus Gallego Arias
2019-02-22
overlay for Equations
Enrico Tassi
2019-02-17
Separate variance and universe fields in inductives.
Gaëtan Gilbert
2019-02-12
[tactics] Remove dependency of abstract on global proof state.
Emilio Jesus Gallego Arias
2019-02-08
Update overlay file
Matthieu Sozeau
2019-02-08
Add overlay for Equations
Matthieu Sozeau
2019-02-08
Add overlays for unicoq and mtac2
Matthieu Sozeau
2019-02-05
Overlays
Maxime Dénès
2019-02-04
Overlays.
Maxime Dénès
2019-01-24
Add Overlays
Maxime Dénès
2018-12-17
Merge PR #9153: [api] Move reduction modules to `tactics`
Pierre-Marie Pédrot
2018-12-17
Merge PR #9220: Move shallow state logic to the function preparing state for ...
Enrico Tassi
2018-12-14
[proof] Rework proof interface.
Emilio Jesus Gallego Arias
2018-12-13
Add overlay
Maxime Dénès
2018-12-11
[ci] Clean overlay folder.
Emilio Jesus Gallego Arias
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-12-05
Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`
Pierre-Marie Pédrot
2018-11-30
[vernac] [hooks] Refactor towards optional hooks.
Emilio Jesus Gallego Arias
2018-11-30
[gramlib] Remove `Ploc.t` in favor of `Loc.t`
Emilio Jesus Gallego Arias
2018-11-28
[ltac] Remove aliases already present in the lower layers.
Emilio Jesus Gallego Arias
2018-11-27
Merge PR #8850: Private universes for opaque polymorphic constants.
Matthieu Sozeau
2018-11-24
Merge PR #8933: Make initial evar map argument to check_evars_are_solved opti...
Pierre-Marie Pédrot
2018-11-23
Adding overlay.
Pierre-Marie Pédrot
2018-11-23
Overlay for private polymorphic universes
Gaëtan Gilbert
2018-11-21
Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib
Enrico Tassi
2018-11-21
Add overlay for solve-remaining-evars-initial-arg
Gaëtan Gilbert
2018-11-21
[legacy proof engine] Remove some cruft.
Emilio Jesus Gallego Arias
2018-11-21
[gramlib] [build] Switch make-based system to packed gramlib
Emilio Jesus Gallego Arias
2018-11-20
Merge PR #7925: Clean transparent state
Maxime Dénès
2018-11-19
Merge PR #9003: [vernacextend] Consolidate extension points API
Pierre-Marie Pédrot
2018-11-19
Merge PR #8902: [ltac] Use CAst nodes in the tactic AST.
Pierre-Marie Pédrot
2018-11-19
Adding overlays.
Pierre-Marie Pédrot
2018-11-18
Merge PR #9018: [devtools] Small script to setup overlays automatically
Gaëtan Gilbert
2018-11-17
[vernacextend] Consolidate extension points API
Emilio Jesus Gallego Arias
2018-11-17
[ci] Cleanup of old overlays.
Emilio Jesus Gallego Arias
2018-11-17
[CoqProject] Abstract warning function for CoqProject readers.
Emilio Jesus Gallego Arias
2018-11-17
[ltac] Use CAst nodes in the tactic AST.
Emilio Jesus Gallego Arias
2018-11-16
Remove the implicit tactic feature following #7229.
Pierre-Marie Pédrot
2018-11-09
Adding an overlay for #8601.
Pierre-Marie Pédrot
2018-11-06
Add overlay for Equations
Matthieu Sozeau
2018-11-05
Merge PR #8515: Command driven attributes
Pierre-Marie Pédrot
2018-11-03
Merge PR #8844: Move abstract out of tactics.ml
Pierre-Marie Pédrot
2018-11-02
Add overlays (command driven attributes)
Gaëtan Gilbert
2018-10-31
Merge PR #8688: Generalizing the various evar_map printers in Termops over an...
Pierre-Marie Pédrot
2018-10-30
Merge PR #8750: [ci] [doc] Notes about branch names.
Gaëtan Gilbert
2018-10-30
Overlays (#8844 split-tactics)
Gaëtan Gilbert
2018-10-30
Adding overlay for coq-elpi
Hugo Herbelin
2018-10-26
Fix overlay for this extension of the PR. To be removed.
Matthieu Sozeau
[prev]
[next]