index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
/
comAssumption.ml
Commit message (
Expand
)
Author
Age
*
universes_of_constr don't include universes of monomorphic constants
Gaëtan Gilbert
2018-06-26
*
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
*
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
*
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-05-17
*
[api] Remove dependency of library on Vernacexpr.
Emilio Jesus Gallego Arias
2018-04-06
*
Rename some universe minimizing "normalize" functions to "minimize"
Gaëtan Gilbert
2018-03-06
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
|
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
2017-12-17