aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
* Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\
| * Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-24
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Gravatar Maxime Dénès2017-11-24
|\
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* kernel: bugfix in filter_stack_domain.Gravatar Matthieu Sozeau2017-07-26
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\
| * Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | This fix is probably not enough to justify that there are no problems withGravatar Maxime Dénès2016-03-04
* | | CLEANUP: Simplifying the changes done in "kernel/*"Gravatar Matej Kosik2016-02-15
* | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \
| * | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | | Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
|/ / /
* | | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
* | | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | | Contracting one extra beta-redex on the fly when typing branches of "match".Gravatar Hugo Herbelin2015-12-05
* | | A few renaming and simplification in inductive.ml.Gravatar Hugo Herbelin2015-12-05
|/ /
* | 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
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 04:49:25 +0000