| Commit message (Expand) | Author | Age |
|---|
| * | Use kernel conversion on terms that contain universe variables during unifica... |  Matthieu Sozeau | 2014-07-20 |
| * | Properly add a Set lower bound on any polymorphic inductive in Type with | Matthieu Sozeau | 2014-07-11 |
| * | Overlooked to remove a change in kernel/closure that made reducing under |  Matthieu Sozeau | 2014-07-10 |
| * | Fixing the previous patch to keep transparent states in sync. |  Pierre-Marie Pédrot | 2014-07-09 |
| * | Recovering transparent state from kernel oracles in constant time. | Pierre-Marie Pédrot | 2014-07-09 |
| * | In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M... | Matthieu Sozeau | 2014-07-07 |
| * | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | 2014-07-03 |
| * | Properly compute the transitive closure of the system of constraints | Matthieu Sozeau | 2014-07-03 |
| * | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau | 2014-07-03 |
| * | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
| * | Quickly fixing bug #2996: typing functions now check when referring to |  Hugo Herbelin | 2014-06-28 |
| * | all coqide specific files moved into ide/ |  Enrico Tassi | 2014-06-25 |
| * | Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_... | Matthieu Sozeau | 2014-06-25 |
| * | Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344) | Enrico Tassi | 2014-06-23 |
| * | Less ocaml warnings. | Hugo Herbelin | 2014-06-21 |
| * | Fix computation of inductive level in monomorphism + indices-matter mode. | Matthieu Sozeau | 2014-06-20 |
| * | Code factorization in LMap. | Pierre-Marie Pédrot | 2014-06-18 |
| * | Fix a destArity that does not exactly match isArity in presence of let-ins. | Matthieu Sozeau | 2014-06-17 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| * | - Fix the de Bruijn problem in check_projection for good :) | Matthieu Sozeau | 2014-06-17 |
| * | Fix a de Bruijn bug in checking code of projections. | Matthieu Sozeau | 2014-06-17 |
| * | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau | 2014-06-17 |
| * | Preemptively remove files from native compilation. |  Guillaume Melquiond | 2014-06-16 |
| * | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin | 2014-06-13 |
| * | Code cleaning in Univ. | Pierre-Marie Pédrot | 2014-06-12 |
| * | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau | 2014-06-11 |
| * | Fixing Sorting Universes in a world where le and lt constraints may be | Pierre-Marie Pédrot | 2014-06-10 |
| * | Compute the trace of a universe inconsistency only when explicitly required | Pierre-Marie Pédrot | 2014-06-10 |
| * | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot | 2014-06-10 |
| * | Specialize the type of [Univ.compare_neq] so that it is clear it is only used | Pierre-Marie Pédrot | 2014-06-10 |
| * | Imperatively check touched universes in compare_neq functions. This ensures | Pierre-Marie Pédrot | 2014-06-10 |
| * | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau | 2014-06-10 |
| * | Oops, one refactoring was not compiled. | Matthieu Sozeau | 2014-06-10 |
| * | More cleanup/reorganizing of univ.ml to separate constraint/universe handling... | Matthieu Sozeau | 2014-06-10 |
| * | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
| * | Remove unused function in univ | Matthieu Sozeau | 2014-06-10 |
| * | Flattening Level module structure in Univ. | Pierre-Marie Pédrot | 2014-06-09 |
| * | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi | 2014-06-08 |
| * | Function in Univ uselessly exported. | Pierre-Marie Pédrot | 2014-06-08 |
| * | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot | 2014-06-07 |
| * | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
| * | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
| * | Dedicated map module for type universes. It uses hashmaps, which are | Pierre-Marie Pédrot | 2014-06-05 |
| * | Removing dead code from Univ. | Pierre-Marie Pédrot | 2014-06-05 |
| * | - 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-04 |
| * | Fixing incorrect printf format. | Pierre-Marie Pédrot | 2014-06-02 |
| * | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau | 2014-05-28 |
| * | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
| * | Update infer_conv to record trivial Prop <= Type i constraints that are neede... | Matthieu Sozeau | 2014-05-26 |
Matthieu Sozeau
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Enrico Tassi
Guillaume Melquiond