index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
vernac.mllib
Age
Commit message (
Expand
)
Author
2019-05-21
[loadpath] Make loadpath handling self-contained and move to vernac
Emilio Jesus Gallego Arias
2019-04-10
Remove calls to Global.env and Libobject from Recordops
Maxime Dénès
2019-04-10
Functionalize env in type classes
Maxime Dénès
2018-11-13
[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.
Emilio Jesus Gallego Arias
2018-11-02
Make attributes more general to make defining #[universes(...)] easy
Gaëtan Gilbert
2018-11-02
Move attributes out of vernacinterp to new attributes module
Gaëtan Gilbert
2018-06-12
[api] Add compatiblity Misctypes module.
Emilio Jesus Gallego Arias
2018-05-27
[api] Make `vernac/` self-contained.
Emilio Jesus Gallego Arias
2018-05-27
[api] [parsing] Move Egram* to `vernac/`
Emilio Jesus Gallego Arias
2017-12-17
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
2017-11-19
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
2017-10-10
[vernac] Remove "Proof using" hacks from parser.
Emilio Jesus Gallego Arias
2017-06-20
[vernac] Remove forward hooks from Obligations.
Emilio Jesus Gallego Arias
2017-04-12
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
