| Commit message (Expand) | Author | Age |
|---|
| * | Move to a representation of universe polymorphic constants using indices for ... |  Matthieu Sozeau | 2014-08-03 |
| * | A tentative uniform naming policy in module Inductiveops. |  Hugo Herbelin | 2014-08-01 |
| * | Useless export of Instance.eqeq. We hashcons everything before calling this |  Pierre-Marie Pédrot | 2014-07-31 |
| * | Optimize check of new subterm relation on match. |  Maxime Dénès | 2014-07-31 |
| * | Fix dynamic computation of recargs for mutual inductives. | Maxime Dénès | 2014-07-31 |
| * | Avoid hconsing instances during appends and conversions from/to arrays. |  Matthieu Sozeau | 2014-07-30 |
| * | Fix eta-conversion code which was failing in nested cases. Fixes bug #3429. | Matthieu Sozeau | 2014-07-29 |
| * | - Do module substitution inside mind_record. | Matthieu Sozeau | 2014-07-25 |
| * | Minor cleaning. | Maxime Dénès | 2014-07-22 |
| * | Revert "Extend subterm relation to pattern matching in return predicates." | Maxime Dénès | 2014-07-22 |
| * | Revert "Propagate size info through pattern matching in predicates, for the" | Maxime Dénès | 2014-07-22 |
| * | Propagate size info through pattern matching in predicates, for the | Maxime Dénès | 2014-07-22 |
| * | Extend subterm relation to pattern matching in return predicates. | Maxime Dénès | 2014-07-22 |
| * | Fix check_inductive_codomain. | Maxime Dénès | 2014-07-22 |
| * | Refine check_is_subterm. | Maxime Dénès | 2014-07-22 |
| * | Refined guard condition of cofixpoints, to anticipate potential futur | Maxime Dénès | 2014-07-22 |
| * | First attempt at a fix for guard condition on cofixpoints. | Maxime Dénès | 2014-07-22 |
| * | Typo in comment. | Maxime Dénès | 2014-07-22 |
| * | Made intersection on regular trees less intensional. | Maxime Dénès | 2014-07-22 |
| * | Refining match subterm and commutative cut rules. The parameters that are | Maxime Dénès | 2014-07-22 |
| * | Tentative fix for the commutative cut subterm rule. | Maxime Dénès | 2014-07-22 |
| * | Tentative patch for incompatibility between subterm relation and dependent | Maxime Dénès | 2014-07-22 |
| * | Universe level maps use HMaps. | Pierre-Marie Pédrot | 2014-07-21 |
| * | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau | 2014-07-21 |
| * | Cleanup code for constant equality in kernel conversion. | Matthieu Sozeau | 2014-07-21 |
| * | 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 |
Matthieu Sozeau
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Enrico Tassi
Guillaume Melquiond