index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
locality.ml
Age
Commit message (
Expand
)
Author
2020-05-18
[declare] Merge `DeclareObl` into `Declare`
Emilio Jesus Gallego Arias
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-10-14
Use kernel info from Global for Lib.sections_{depth,are_opened}
Gaëtan Gilbert
2019-06-24
[api] [proof] Move `discharge` type to vernac_ast where it is used.
Emilio Jesus Gallego Arias
2019-06-24
[api] Move `locality` from `library` to `vernac`.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-08
Cleaning the status of Local Definition and similar.
Hugo Herbelin
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-29
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-22
[plugin] Remove LocalityFixme über hack.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
