aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
Commit message (Expand)AuthorAge
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* improve efficiency of the reduction interpreter of coqtopGravatar Bruno Barras2015-01-06
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Gravatar Matthieu Sozeau2014-07-29
* Overlooked to remove a change in kernel/closure that made reducing underGravatar Matthieu Sozeau2014-07-10
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing coqchk. It was my fault, I misused canonical and user equalitiesGravatar Pierre-Marie Pédrot2014-04-04
* Small optimizations in Closure:Gravatar Pierre-Marie Pédrot2014-02-09
* Do not overallocate closures' named environments in infos. Modifying the accessGravatar Pierre-Marie Pédrot2013-12-15
* Slightly more efficient zip function in Closure.Gravatar Pierre-Marie Pédrot2013-11-24
* Small allocation improvement in Closure.Gravatar Pierre-Marie Pédrot2013-11-23
* Using allocation-free version of Array higher-order function in criticalGravatar ppedrot2013-11-04
* Closure: fix an issue with r16959 spotted by MatthieuGravatar letouzey2013-11-02
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Avoiding useless allocations in Closure.Gravatar ppedrot2013-10-31
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Small optimization in Closure: replaced an index list with an array.Gravatar ppedrot2012-12-08
* Kernel/closure: add eta red_kindGravatar pboutill2012-11-28
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Noise for nothingGravatar pboutill2012-03-02
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24