aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
* Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
* Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
* Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* Fix my previous commit on ~polypropGravatar Pierre Letouzey2015-05-12
* Extraction: fix the detection of the "polyprop" situationGravatar Pierre Letouzey2015-05-12
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Relax a bit the guard condition.Gravatar Maxime Dénès2014-08-06
* One more optimization for guard checking of cofixpoints.Gravatar Maxime Dénès2014-08-04
* More optimization in guard checking.Gravatar Maxime Dénès2014-08-04
* Fix an exponential behavior in guard checker for cofixpoints.Gravatar Maxime Dénès2014-08-04
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Optimize check of new subterm relation on match.Gravatar Maxime Dénès2014-07-31
* Fix dynamic computation of recargs for mutual inductives.Gravatar Maxime Dénès2014-07-31
* Minor cleaning.Gravatar Maxime Dénès2014-07-22
* Revert "Extend subterm relation to pattern matching in return predicates."Gravatar Maxime Dénès2014-07-22
* Revert "Propagate size info through pattern matching in predicates, for the"Gravatar Maxime Dénès2014-07-22
* Propagate size info through pattern matching in predicates, for theGravatar Maxime Dénès2014-07-22
* Extend subterm relation to pattern matching in return predicates.Gravatar Maxime Dénès2014-07-22
* 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
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Avoid allocations in type_of_inductiveGravatar Matthieu Sozeau2014-05-08
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 21:31:14 +0000