aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
Commit message (Expand)AuthorAge
* 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
* 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
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Fix bug when defining primitive projections mixing defined and abstracts fields.Gravatar Matthieu Sozeau2014-08-29
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:18:29 +0000