aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2015-02-11Fixing bug #4019, and checker blow-up at once.Pierre-Marie Pédrot
2015-02-11Clarifying the implementation of universe hashconsing.Pierre-Marie Pédrot
2015-02-10Fix typeops ignoring results of check functions with let _, and oneMatthieu Sozeau
2015-02-04Nativelib: catch Unix_error (like no ocamlopt found)Enrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-28Fixing bug #3931.Pierre-Marie Pédrot
2015-01-20Fix a critical bug in machine arithmetic for native compiler.Maxime Dénès
2015-01-17Fix #3379, now that Require inside modules is allowed again.Maxime Dénès
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-15Make -print-mod-uid accept a list of files.Maxime Dénès
2015-01-13Native compiler: if debug flag not present, remove .native files.Maxime Dénès
2015-01-13Fix bug when discharging universe constraints coming from variablesMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-12Fix a few typos.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-07Aligning printing of universe constraints.Hugo Herbelin
2015-01-06Fix some documentation typos.Guillaume Melquiond
2015-01-06improve efficiency of the reduction interpreter of coqtopBruno Barras
2015-01-06Rename ill-named "imports" field of safe_env into "required".Maxime Dénès
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2014-12-27universes_of_constant: do a proper set union of body and type univsEnrico Tassi
2014-12-27Revert "Term: include a function to print terms"Enrico Tassi
2014-12-26Term: include a function to print termsEnrico Tassi
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-12-21Dead code in Univ.Pierre-Marie Pédrot
2014-12-18Cleaning up universe list implementation in Univ.Pierre-Marie Pédrot
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-17Fix (actually, properly implement :) hashconsing of projections,Matthieu Sozeau
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-12-15Fix treatment of universe context in typecheck inductive (was addedMatthieu Sozeau
2014-12-14Fix merging of name maps in union of universe contexts.Matthieu Sozeau
2014-12-10Revert commit that inverted the preference for FFlex/FProj problems inMatthieu Sozeau
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-23Fix #3824. de Bruijn error in normalization of fixpoints.Maxime Dénès
2014-11-21Fix bug #3804.Matthieu Sozeau
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-11-19Slightly improving error messages when mismatch with Proof using at Qed time.Hugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-11-10Fix #3282: VM confused by let bindings in fixpoints.Maxime Dénès
2014-11-10Better printing of dynlink errors in native compiler.Maxime Dénès
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-24Remove an ununsed pattern and commented code in the kernel.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:52:22 +0000