index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
/
classes.ml
Commit message (
Expand
)
Author
Age
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
*
Move interning the [hint_pattern] outside the Typeclasses hooks.
Gaëtan Gilbert
2018-05-30
*
Merge PR #7558: [api] Make `vernac/` self-contained.
Maxime Dénès
2018-05-30
|
\
|
*
[tactics] Turn boolean locality hint parameter into a named one.
Emilio Jesus Gallego Arias
2018-05-27
*
|
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
|
/
*
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-05-17
*
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Pierre-Marie Pédrot
2018-05-04
|
\
*
\
Merge PR #6935: Separate universe minimization and evar normalization functions
Pierre-Marie Pédrot
2018-04-30
|
\
\
|
|
*
[api] Move `hint_info_expr` to `Typeclasses`.
Emilio Jesus Gallego Arias
2018-04-26
|
|
/
|
/
|
*
|
Merge PR #7152: [api] Remove dependency of library on Vernacexpr.
Pierre-Marie Pédrot
2018-04-23
|
\
\
|
|
*
Deprecate mixing univ minimization and evm normalization functions.
Gaëtan Gilbert
2018-04-17
|
|
/
|
/
|
|
*
[api] Remove dependency of library on Vernacexpr.
Emilio Jesus Gallego Arias
2018-04-06
*
|
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-03-31
|
/
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)
Maxime Dénès
2018-03-07
|
\
|
*
Sanitize universe declaration in Context (stop using a ref...)
Gaëtan Gilbert
2018-03-05
*
|
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
|
|
/
|
/
|
*
|
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Maxime Dénès
2018-03-04
|
\
\
*
\
\
Merge PR #6676: [proofview] goals come with a state
Maxime Dénès
2018-03-04
|
\
\
\
|
|
*
|
[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
|
*
proofview: goals come with a state
Enrico Tassi
2018-02-20
|
/
*
Remove the local polymorphic flag hack.
Maxime Dénès
2017-12-27
*
Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...
Maxime Dénès
2017-12-27
|
\
*
|
[flags] Make program_mode a parameter for commands in vernac.
Emilio Jesus Gallego Arias
2017-12-17
*
|
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
2017-12-17
*
|
[econstr] Switch constrintern API to non-imperative style.
Emilio Jesus Gallego Arias
2017-12-15
*
|
[econstr] Cleanup in `vernac/classes.ml`.
Emilio Jesus Gallego Arias
2017-12-13
*
|
Fix #6323: stronger restrict universe context vs abstract.
Gaëtan Gilbert
2017-12-06
*
|
Cleanup API for registering universe binders.
Matthieu Sozeau
2017-12-01
|
*
Remove unused boolean from cl_context field of Typeclasses.typeclass
Gaëtan Gilbert
2017-11-30
|
/
*
Fix #5347: unify declaration of axioms with and without bound univs.
Gaëtan Gilbert
2017-11-25
*
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
Separate checking univ_decls and obtaining universe binder names.
Gaëtan Gilbert
2017-11-24
*
Use Maps and ids for universe binders
Gaëtan Gilbert
2017-11-24
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
*
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
*
Make the typeclass implementation fully compatible with universe polymorphism.
Pierre-Marie Pédrot
2017-07-13
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[vernac] Remove forward hooks from Obligations.
Emilio Jesus Gallego Arias
2017-06-20
*
Squashed commit of the following:
Amin Timany
2017-06-16
[next]