aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.ml
Commit message (Expand)AuthorAge
* Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\
* | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
* | Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \
| | * Handle mutual record at the vernac level.Gravatar Pierre-Marie Pédrot2018-06-24
| |/ |/|
* | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| * Existing Class noop when already a class + warning.Gravatar Gaëtan Gilbert2018-06-08
|/
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
| * Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* | [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
|/
* Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
* Fixing the 3 cases of a "Stream.Error" ended with two periods.Gravatar Hugo Herbelin2018-04-12
* Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-03-08
* Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
* | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/ /
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* | Remove unused argument in Record.declare_structureGravatar Gaëtan Gilbert2018-02-14
| * Fixing an anomaly in the presence of "let-in" in the type of a record.Gravatar Hugo Herbelin2018-02-13
|/
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* Inference of inductive subtyping does not need an evar map.Gravatar Gaëtan Gilbert2018-02-10
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Gravatar Maxime Dénès2017-12-27
|\
* \ Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Gravatar Maxime Dénès2017-12-27
|\ \
| | * [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |/ |/|
* | [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
* | [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
* | Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
| * Remove unused boolean from cl_context field of Typeclasses.typeclassGravatar Gaëtan Gilbert2017-11-30
|/
* Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* Fix defining non primitive projections with abstracted universes.Gravatar Gaëtan Gilbert2017-11-24
* Register universe binders for record projections.Gravatar Gaëtan Gilbert2017-11-24
* Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
* Use Maps and ids for universe bindersGravatar Gaëtan Gilbert2017-11-24
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Removing dead code which raised questions.Gravatar Hugo Herbelin2017-10-24
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Gravatar Maxime Dénès2017-10-20
|\
| * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
* Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13
* Getting rid of AUContext abstraction breakers in Record.Gravatar Pierre-Marie Pédrot2017-07-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 10:14:48 +0000