aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-09-01Coqide prints succesive hyps of the same type on 1 linePierre Boutillier
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-18Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-13Small optimization in Cooking: do not construct identity substitutions.Pierre-Marie Pédrot
2014-08-09Adding a primitive to merge ContextSets which is more efficient when onePierre-Marie Pédrot
2014-08-09Cleaning up interface of ContextSet.Pierre-Marie Pédrot
2014-08-06Relax a bit the guard condition.Maxime Dénès
2014-08-05make a few lines fit the screenEnrico Tassi
2014-08-04One more optimization for guard checking of cofixpoints.Maxime Dénès
2014-08-04More optimization in guard checking.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:38:17 +0000