aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* universes_of_constant: do a proper set union of body and type univsGravatar Enrico Tassi2014-12-27
* Revert "Term: include a function to print terms"Gravatar Enrico Tassi2014-12-27
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Dead code in Univ.Gravatar Pierre-Marie Pédrot2014-12-21
* Cleaning up universe list implementation in Univ.Gravatar Pierre-Marie Pédrot2014-12-18
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
* Fix treatment of universe context in typecheck inductive (was addedGravatar Matthieu Sozeau2014-12-15
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Revert commit that inverted the preference for FFlex/FProj problems inGravatar Matthieu Sozeau2014-12-10
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Fix #3824. de Bruijn error in normalization of fixpoints.Gravatar Maxime Dénès2014-11-23
* Fix bug #3804.Gravatar Matthieu Sozeau2014-11-21
* Exporting the function handling side-effects only applied to terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Slightly improving error messages when mismatch with Proof using at Qed time.Gravatar Hugo Herbelin2014-11-19
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Cleaner interfaces for linking locations of native compiler.Gravatar Maxime Dénès2014-11-12
* Fix #3282: VM confused by let bindings in fixpoints.Gravatar Maxime Dénès2014-11-10
* Better printing of dynlink errors in native compiler.Gravatar Maxime Dénès2014-11-10
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:22:01 +0000