aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
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
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-19Array.create is deprecatedpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:02:52 +0000