index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
/
record.ml
Commit message (
Expand
)
Author
Age
*
Merge PR #7866: Implementation of mutual records in the higher strata
Maxime Dénès
2018-06-28
|
\
*
|
Remove Sorts.contents
Gaëtan Gilbert
2018-06-26
*
|
Merge PR #7559: Existing Class noop when already a class + warning.
Matthieu Sozeau
2018-06-25
|
\
\
|
|
*
Handle mutual record at the vernac level.
Pierre-Marie Pédrot
2018-06-24
|
|
/
|
/
|
*
|
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-23
*
|
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
|
*
Existing Class noop when already a class + warning.
Gaëtan Gilbert
2018-06-08
|
/
*
[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
*
Merge PR #7384: Split Universes
Pierre-Marie Pédrot
2018-05-22
|
\
|
*
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-05-17
*
|
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
|
/
*
Deprecate mixing univ minimization and evm normalization functions.
Gaëtan Gilbert
2018-04-17
*
Fixing the 3 cases of a "Stream.Error" ended with two periods.
Hugo Herbelin
2018-04-12
*
Fix error with univ binders on monomorphic records.
Gaëtan Gilbert
2018-03-08
*
Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...
Maxime Dénès
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
*
|
Remove unused argument in Record.declare_structure
Gaëtan Gilbert
2018-02-14
|
*
Fixing an anomaly in the presence of "let-in" in the type of a record.
Hugo Herbelin
2018-02-13
|
/
*
Use specialized function for inductive subtyping inference.
Gaëtan Gilbert
2018-02-11
*
Inference of inductive subtyping does not need an evar map.
Gaëtan Gilbert
2018-02-10
*
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
*
Returning instance instead of substitution in universe context abstraction.
Pierre-Marie Pédrot
2017-12-30
*
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
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
|
\
\
|
|
*
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
|
|
/
|
/
|
*
|
[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
*
|
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
|
/
*
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
*
Fix defining non primitive projections with abstracted universes.
Gaëtan Gilbert
2017-11-24
*
Register universe binders for record projections.
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] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
[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
*
Removing dead code which raised questions.
Hugo Herbelin
2017-10-24
*
Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...
Maxime Dénès
2017-10-20
|
\
|
*
Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).
Hugo Herbelin
2017-10-05
*
|
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
*
More precise type for universe entries.
Pierre-Marie Pédrot
2017-07-26
*
Make the typeclass implementation fully compatible with universe polymorphism.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Record.
Pierre-Marie Pédrot
2017-07-13
[next]