index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
comAssumption.ml
Age
Commit message (
Expand
)
Author
2018-11-09
Adding universe names to polymorphic entry instances.
Pierre-Marie Pédrot
2018-10-16
{Univops -> Vars}.universes_of_constr
Gaëtan Gilbert
2018-10-16
UnivGen.constr_of_glob_univ -> Constr.mkRef
Gaëtan Gilbert
2018-10-05
Using smart mkLambdaCN/mkProdCN.
Hugo Herbelin
2018-06-26
universes_of_constr don't include universes of monomorphic constants
Gaëtan Gilbert
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-25
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-17
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-04-06
[api] Remove dependency of library on Vernacexpr.
Emilio Jesus Gallego Arias
2018-03-06
Rename some universe minimizing "normalize" functions to "minimize"
Gaëtan Gilbert
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-02-28
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2017-12-17
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
