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
2020-01-30
Merge PR #11307: Remove the hacks relying on hardwired libobject tags.
Maxime Dénès
2019-12-22
Rename files with Class in their name to make their role clearer.
Pierre-Marie Pédrot
2019-12-22
Remove the hacks relying on hardwired libobject tags.
Pierre-Marie Pédrot
2019-10-31
[prettyp] remove `mod_ops` and `indirect_accessor` parameters
Gaëtan Gilbert
2019-10-31
Move prettyp (Print implementation) to vernac/
Gaëtan Gilbert
2019-10-31
Move Arguments implementation to its own file (from vernacentries)
Gaëtan Gilbert
2019-10-24
[declare] Split inductive declaration code to vernac/
Emilio Jesus Gallego Arias
2019-10-24
[declare] Split universe declaration code to vernac/
Emilio Jesus Gallego Arias
2019-10-13
Merge PR #10670: ComAssumption cleanup
Pierre-Marie Pédrot
2019-10-07
[vernac] Split vernacular translation and interpretation.
Emilio Jesus Gallego Arias
2019-10-05
Move do_primitive from comassumption to its own module.
Gaëtan Gilbert
2019-09-18
[library] Move `Declaremods` to `vernac/`
Emilio Jesus Gallego Arias
2019-08-30
[library] Move library to vernac
Emilio Jesus Gallego Arias
2019-07-08
Merge PR #10497: [lemmas] Move mutually recursive lemma analysis to its own m...
Gaëtan Gilbert
2019-07-07
[lemmas] Move mutually recursive lemma analysis to its own module.
Emilio Jesus Gallego Arias
2019-07-07
[error] Remove special error printing pre-processing
Emilio Jesus Gallego Arias
2019-06-17
[proof] Remove terminator type, unifying regular and obligation ones.
Emilio Jesus Gallego Arias
2019-06-17
[proof] Move declaration hooks to DeclareDef.
Emilio Jesus Gallego Arias
2019-06-17
[proof] Unify obligation proof save path: Part I, declareObl
Emilio Jesus Gallego Arias
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
