aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Univs: Fix bug #4726Gravatar Matthieu Sozeau2016-06-29
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \
| * | Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* | | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-20
|\| |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\ \ \
| | * | Fix bug #4627: records with no declared arity can be template polymorphic.Gravatar Matthieu Sozeau2016-03-17
| |/ /
| * | Fix bug when a sort is ascribed to a RecordGravatar Matthieu Sozeau2016-03-15
* | | Renaming variants of Entries.local_entryGravatar Matej Kosik2016-02-16
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* | | | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| * | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ / /
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \
| * | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
|/ / /
* / / Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
|/ /
* | Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | Univs: fix inference of the lowest sort for records.Gravatar Matthieu Sozeau2015-10-02
* | Univs: correcly compute the levels of records when they fall in Prop.Gravatar Matthieu Sozeau2015-10-02
* | Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* | Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * Add corresponding field in `VernacInductive`.Gravatar Arnaud Spiwack2015-06-24
| * Add a corresponding field in `mutual_inductive_entry` (part 1).Gravatar Arnaud Spiwack2015-06-24
|/
* Fixing bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 18:33:13 +0000