aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2015-03-13Fix compilation with forthcoming Ocaml version 4.03.Arnaud Spiwack
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-24New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Arnaud Spiwack
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-21Import (module): Do not force constraints if not ready (Close #4066)Enrico Tassi
2015-02-14Univs: When computing the level of an inductive including indices, letsMatthieu Sozeau
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:25:27 +0000