aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fixing bug #3931.Gravatar Pierre-Marie Pédrot2015-01-28
* Fix a critical bug in machine arithmetic for native compiler.Gravatar Maxime Dénès2015-01-20
* Fix #3379, now that Require inside modules is allowed again.Gravatar Maxime Dénès2015-01-17
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Make -print-mod-uid accept a list of files.Gravatar Maxime Dénès2015-01-15
* Native compiler: if debug flag not present, remove .native files.Gravatar Maxime Dénès2015-01-13
* Fix bug when discharging universe constraints coming from variablesGravatar Matthieu Sozeau2015-01-13
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix a few typos.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Aligning printing of universe constraints.Gravatar Hugo Herbelin2015-01-07
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* improve efficiency of the reduction interpreter of coqtopGravatar Bruno Barras2015-01-06
* Rename ill-named "imports" field of safe_env into "required".Gravatar Maxime Dénès2015-01-06
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 08:12:15 +0000