aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
* Fix check_inductive_codomain.Gravatar Maxime Dénès2014-07-22
* Refine check_is_subterm.Gravatar Maxime Dénès2014-07-22
* Refined guard condition of cofixpoints, to anticipate potential futurGravatar Maxime Dénès2014-07-22
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* Typo in comment.Gravatar Maxime Dénès2014-07-22
* Made intersection on regular trees less intensional.Gravatar Maxime Dénès2014-07-22
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
* Tentative fix for the commutative cut subterm rule.Gravatar Maxime Dénès2014-07-22
* Tentative patch for incompatibility between subterm relation and dependentGravatar Maxime Dénès2014-07-22
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
* Cleanup code for constant equality in kernel conversion.Gravatar Matthieu Sozeau2014-07-21
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Properly add a Set lower bound on any polymorphic inductive in Type withGravatar Matthieu Sozeau2014-07-11
* Overlooked to remove a change in kernel/closure that made reducing underGravatar Matthieu Sozeau2014-07-10
* Fixing the previous patch to keep transparent states in sync.Gravatar Pierre-Marie Pédrot2014-07-09
* Recovering transparent state from kernel oracles in constant time.Gravatar Pierre-Marie Pédrot2014-07-09
* In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...Gravatar Matthieu Sozeau2014-07-07
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...Gravatar Matthieu Sozeau2014-06-25
* Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-03 21:31:32 +0000