aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
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
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-04-10Fix guard condition for nested cofixpoints.Maxime Dénès
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
2014-01-15Christmas is over...Maxime Dénès
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Matthieu Sozeau
2013-10-24inductive.ml : get rid of some obvious (Lazy.force (lazy t))letouzey
2013-10-24Rtree : cleanup of the comparing codeletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:36:03 +0000