aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
* Fix retroknowledge for int31 division.Gravatar Maxime Dénès2014-10-24
* No hash consing across calls to the native compiler.Gravatar Maxime Dénès2014-10-24
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Gravatar Matthieu Sozeau2014-10-14
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Move eta-expansion after delta reduction in kernel reduction. This makesGravatar Matthieu Sozeau2014-10-02
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Make the retroknowledge marshalable.Gravatar Arnaud Spiwack2014-09-24
* Clean a bit of univ.ml, add credits.Gravatar Matthieu Sozeau2014-09-18
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...Gravatar Matthieu Sozeau2014-08-18
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Small optimization in Cooking: do not construct identity substitutions.Gravatar Pierre-Marie Pédrot2014-08-13
* Adding a primitive to merge ContextSets which is more efficient when oneGravatar Pierre-Marie Pédrot2014-08-09
* Cleaning up interface of ContextSet.Gravatar Pierre-Marie Pédrot2014-08-09
* Relax a bit the guard condition.Gravatar Maxime Dénès2014-08-06
* make a few lines fit the screenGravatar Enrico Tassi2014-08-05
* One more optimization for guard checking of cofixpoints.Gravatar Maxime Dénès2014-08-04
* More optimization in guard checking.Gravatar Maxime Dénès2014-08-04
* Fix an exponential behavior in guard checker for cofixpoints.Gravatar Maxime Dénès2014-08-04
* Fixing semantics of Univ.Level.equal.Gravatar Pierre-Marie Pédrot2014-08-04
* Fix infer conv using the wrong universe conversion flexibility informationGravatar Matthieu Sozeau2014-08-03
* - Fix handling of opaque polymorphic definitions which were turned transparent.Gravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
* Optimize check of new subterm relation on match.Gravatar Maxime Dénès2014-07-31
* Fix dynamic computation of recargs for mutual inductives.Gravatar Maxime Dénès2014-07-31
* Avoid hconsing instances during appends and conversions from/to arrays.Gravatar Matthieu Sozeau2014-07-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:31:36 +0000