aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
...
| * Add a flag to deactivate guard checking in the kernel.Gravatar Arnaud Spiwack2015-06-26
|/
* 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
* Fix guard condition for nested cofixpoints.Gravatar Maxime Dénès2014-04-10
* Relaxing the sort elimination check to allow for let-bindings in arities.Gravatar Maxime Dénès2014-01-18
* Christmas is over...Gravatar Maxime Dénès2014-01-15
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Gravatar Matthieu Sozeau2013-12-17
* inductive.ml : get rid of some obvious (Lazy.force (lazy t))Gravatar letouzey2013-10-24
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 02:13:23 +0000