aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Univs: When computing the level of an inductive including indices, letsGravatar Matthieu Sozeau2015-02-14
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Fix typeops ignoring results of check functions with let _, and oneGravatar Matthieu Sozeau2015-02-10
* Nativelib: catch Unix_error (like no ocamlopt found)Gravatar Enrico Tassi2015-02-04
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 17:38:31 +0000