aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-21
* Fix computation of inductive level in monomorphism + indices-matter mode.Gravatar Matthieu Sozeau2014-06-20
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
* Fix a destArity that does not exactly match isArity in presence of let-ins.Gravatar Matthieu Sozeau2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
* Fix a de Bruijn bug in checking code of projections.Gravatar Matthieu Sozeau2014-06-17
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* Preemptively remove files from native compilation.Gravatar Guillaume Melquiond2014-06-16
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
* Code cleaning in Univ.Gravatar Pierre-Marie Pédrot2014-06-12
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Fixing Sorting Universes in a world where le and lt constraints may beGravatar Pierre-Marie Pédrot2014-06-10
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
* Specialize the type of [Univ.compare_neq] so that it is clear it is only usedGravatar Pierre-Marie Pédrot2014-06-10
* Imperatively check touched universes in compare_neq functions. This ensuresGravatar Pierre-Marie Pédrot2014-06-10
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* Oops, one refactoring was not compiled.Gravatar Matthieu Sozeau2014-06-10
* More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Remove unused function in univGravatar Matthieu Sozeau2014-06-10
* Flattening Level module structure in Univ.Gravatar Pierre-Marie Pédrot2014-06-09
* ind_tables: always declare side effects (Closes: HOTT#110)Gravatar Enrico Tassi2014-06-08
* Function in Univ uselessly exported.Gravatar Pierre-Marie Pédrot2014-06-08
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* Dedicated map module for type universes. It uses hashmaps, which areGravatar Pierre-Marie Pédrot2014-06-05
* Removing dead code from Univ.Gravatar Pierre-Marie Pédrot2014-06-05
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Fixing incorrect printf format.Gravatar Pierre-Marie Pédrot2014-06-02
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Update infer_conv to record trivial Prop <= Type i constraints that are neede...Gravatar Matthieu Sozeau2014-05-26
* Fix native_compute for systems with a limited size for the command line.Gravatar Guillaume Melquiond2014-05-22
* Revert "Decent error message when a constant is not found"Gravatar Enrico Tassi2014-05-16
* Decent error message when a constant is not foundGravatar Enrico Tassi2014-05-16
* Another try at close_proof that should behave better w.r.t. exception handling.Gravatar Matthieu Sozeau2014-05-16
* Rewritten the sorting algorithm for universes with a better complexity.Gravatar Pierre-Marie Pédrot2014-05-13
* Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Gravatar Pierre-Marie Pédrot2014-05-11
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Avoid allocations in type_of_inductiveGravatar Matthieu Sozeau2014-05-08
* Fast-path equality of sorts in compare_constr*Gravatar Matthieu Sozeau2014-05-08
* Add missing case for primitive projection in fold_map.Gravatar Matthieu Sozeau2014-05-06
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* Add doc on the new API for universe polymorphism and primitive projectionsGravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 15:42:16 +0000