aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2014-08-05make a few lines fit the screenEnrico Tassi
2014-08-04One more optimization for guard checking of cofixpoints.Maxime Dénès
2014-08-04More optimization in guard checking.Maxime Dénès
2014-08-04Fix an exponential behavior in guard checker for cofixpoints.Maxime Dénès
2014-08-04Fixing semantics of Univ.Level.equal.Pierre-Marie Pédrot
2014-08-03Fix infer conv using the wrong universe conversion flexibility informationMatthieu Sozeau
2014-08-03- Fix handling of opaque polymorphic definitions which were turned transparent.Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-07-31Useless export of Instance.eqeq. We hashcons everything before calling thisPierre-Marie Pédrot
2014-07-31Optimize check of new subterm relation on match.Maxime Dénès
2014-07-31Fix dynamic computation of recargs for mutual inductives.Maxime Dénès
2014-07-30Avoid hconsing instances during appends and conversions from/to arrays.Matthieu Sozeau
2014-07-29Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Matthieu Sozeau
2014-07-25- Do module substitution inside mind_record.Matthieu Sozeau
2014-07-22Minor cleaning.Maxime Dénès
2014-07-22Revert "Extend subterm relation to pattern matching in return predicates."Maxime Dénès
2014-07-22Revert "Propagate size info through pattern matching in predicates, for the"Maxime Dénès
2014-07-22Propagate size info through pattern matching in predicates, for theMaxime Dénès
2014-07-22Extend subterm relation to pattern matching in return predicates.Maxime Dénès
2014-07-22Fix check_inductive_codomain.Maxime Dénès
2014-07-22Refine check_is_subterm.Maxime Dénès
2014-07-22Refined guard condition of cofixpoints, to anticipate potential futurMaxime Dénès
2014-07-22First attempt at a fix for guard condition on cofixpoints.Maxime Dénès
2014-07-22Typo in comment.Maxime Dénès
2014-07-22Made intersection on regular trees less intensional.Maxime Dénès
2014-07-22Refining match subterm and commutative cut rules. The parameters that areMaxime Dénès
2014-07-22Tentative fix for the commutative cut subterm rule.Maxime Dénès
2014-07-22Tentative patch for incompatibility between subterm relation and dependentMaxime Dénès
2014-07-21Universe level maps use HMaps.Pierre-Marie Pédrot
2014-07-21Cleanup substitution inside universe instances, only done through subst_fn now,Matthieu Sozeau
2014-07-21Cleanup code for constant equality in kernel conversion.Matthieu Sozeau
2014-07-20Use kernel conversion on terms that contain universe variables during unifica...Matthieu Sozeau
2014-07-11Properly add a Set lower bound on any polymorphic inductive in Type withMatthieu Sozeau
2014-07-10Overlooked to remove a change in kernel/closure that made reducing underMatthieu Sozeau
2014-07-09Fixing the previous patch to keep transparent states in sync.Pierre-Marie Pédrot
2014-07-09Recovering transparent state from kernel oracles in constant time.Pierre-Marie Pédrot
2014-07-07In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...Matthieu Sozeau
2014-07-03Cleanup code related to the constraint solving, which sits now outside theMatthieu Sozeau
2014-07-03Properly compute the transitive closure of the system of constraintsMatthieu Sozeau
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Matthieu Sozeau
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-25Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...Matthieu Sozeau
2014-06-23Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Enrico Tassi
2014-06-21Less ocaml warnings.Hugo Herbelin
2014-06-20Fix computation of inductive level in monomorphism + indices-matter mode.Matthieu Sozeau
2014-06-18Code factorization in LMap.Pierre-Marie Pédrot
2014-06-17Fix a destArity that does not exactly match isArity in presence of let-ins.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:11:36 +0000