aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-06-12Code cleaning in Univ.Pierre-Marie Pédrot
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-06-10Fixing Sorting Universes in a world where le and lt constraints may bePierre-Marie Pédrot
2014-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
2014-06-10Made explanations for universe inconsistencies optional. They are only usedPierre-Marie Pédrot
2014-06-10Specialize the type of [Univ.compare_neq] so that it is clear it is only usedPierre-Marie Pédrot
2014-06-10Imperatively check touched universes in compare_neq functions. This ensuresPierre-Marie Pédrot
2014-06-10- Fix substitution of universes which needlessly hashconsed existing universes.Matthieu Sozeau
2014-06-10Oops, one refactoring was not compiled.Matthieu Sozeau
2014-06-10More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-10Remove unused function in univMatthieu Sozeau
2014-06-09Flattening Level module structure in Univ.Pierre-Marie Pédrot
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
2014-06-08Function in Univ uselessly exported.Pierre-Marie Pédrot
2014-06-07Moving a Thread.yield in check_interrupt.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-06-05Dedicated map module for type universes. It uses hashmaps, which arePierre-Marie Pédrot
2014-06-05Removing dead code from Univ.Pierre-Marie Pédrot
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-06-02Fixing incorrect printf format.Pierre-Marie Pédrot
2014-05-28- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someMatthieu Sozeau
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-26Update infer_conv to record trivial Prop <= Type i constraints that are neede...Matthieu Sozeau
2014-05-22Fix native_compute for systems with a limited size for the command line.Guillaume Melquiond
2014-05-16Revert "Decent error message when a constant is not found"Enrico Tassi
2014-05-16Decent error message when a constant is not foundEnrico Tassi
2014-05-16Another try at close_proof that should behave better w.r.t. exception handling.Matthieu Sozeau
2014-05-13Rewritten the sorting algorithm for universes with a better complexity.Pierre-Marie Pédrot
2014-05-11Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Pierre-Marie Pédrot
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-08Avoid allocations in type_of_inductiveMatthieu Sozeau
2014-05-08Fast-path equality of sorts in compare_constr*Matthieu Sozeau
2014-05-06Add missing case for primitive projection in fold_map.Matthieu Sozeau
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Find a more efficient fix for dealing with template universes:Matthieu Sozeau
2014-05-06Add doc on the new API for universe polymorphism and primitive projectionsMatthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06- Fix handling of polymorphic inductive elimination schemes.Matthieu Sozeau
2014-05-06Cleanup in constr, correct classification of polymorphic defs.Matthieu Sozeau
2014-05-06- Fix index-list to show computational relations for rewriting files.Matthieu Sozeau
2014-05-06Various fixes of universe polymorphism and projections when they're set.Matthieu Sozeau
2014-05-06- Fix Check to use the constraints inferred during type inference.Matthieu Sozeau
2014-05-06Improve universe/level comparison using hashes.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 15:04:59 +0000