aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05Contracting one extra beta-redex on the fly when typing branches of "match".Hugo Herbelin
2015-12-05A few renaming and simplification in inductive.ml.Hugo Herbelin
2015-10-12Univs: be more restrictive for template polymorphic constants: onlyMatthieu Sozeau
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-07-15Univs/Inductive: fix typechecking of casesMatthieu Sozeau
2015-07-10Unused variables reported by OCaml.Hugo Herbelin
2015-07-09Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Matthieu Sozeau
2015-07-09Template polymorphism: A bug-fix for Bug #4258mlasson
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-05-12Fix my previous commit on ~polypropPierre Letouzey
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-06Fix some documentation typos.Guillaume Melquiond
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-10Fix generation of inductive elimination principle for primitive records.Matthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-06Relax a bit the guard condition.Maxime Dénès
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-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-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-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-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-08Avoid allocations in type_of_inductiveMatthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:04:32 +0000