aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2014-10-24Fix retroknowledge for int31 division.Maxime Dénès
2014-10-24No hash consing across calls to the native compiler.Maxime Dénès
2014-10-22Pushing Pierre's factorization of names in goal context printing fromHugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-14Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Matthieu Sozeau
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-10-13STM: simplify how the term part of a side effect is retrievedEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Fix segfault in native compiler on int31 division.Maxime Dénès
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-10-02Move eta-expansion after delta reduction in kernel reduction. This makesMatthieu Sozeau
2014-09-30Simplify evarconv thanks to new delta status of projections,Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
2014-09-18Clean a bit of univ.ml, add credits.Matthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-10Fix generation of inductive elimination principle for primitive records.Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of subst_un...Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:28:56 +0000