aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\
| * Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
| * Hashconsing modules.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
| * Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | ADD: Names.Name.is_{anonymous,name}Gravatar Matej Kosik2016-02-18
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-17
|\ \
* | | Term: fix a comment (first de Bruijn index is 1)Gravatar Pierre Letouzey2016-02-16
| * | Renaming variants of Entries.local_entryGravatar Matej Kosik2016-02-16
| * | CLEANUP: Simplifying the changes done in "kernel/*"Gravatar Matej Kosik2016-02-15
| * | REFORMATTING: kernel/context.ml{,i}Gravatar Matej Kosik2016-02-09
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Fixing bde12b70 about reporting ill-formed constructor.Gravatar Hugo Herbelin2016-01-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Universes algorithm : clarified commentsGravatar Jacques-Henri Jourdan2016-01-17
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2016-01-11
* | | COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2016-01-11
| | * Be more verbose about failure to compile libraries to native code.Gravatar Guillaume Melquiond2016-01-08
| | * Fix a misleading comment for substn_varsGravatar Matthieu Sozeau2016-01-07
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\ \ \ | | |/ | |/|
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\| |
| * | Fix handling of side-effects in case of `Opaque side-effects as well.Gravatar Matthieu Sozeau2016-01-04
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | Avoid warnings about loop indices.Gravatar Guillaume Melquiond2016-01-02
* | | Fix typos.Gravatar Guillaume Melquiond2016-01-01
* | | Remove unused open.Gravatar Guillaume Melquiond2016-01-01
| * | Fix bug #4456, anomaly in handle-side effectsGravatar Matthieu Sozeau2015-12-31
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\| |
* | | Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
| | * COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2015-12-22
| | * COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2015-12-22
| |/ |/|
| * Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* | COMMENTS: added to the "Constr.case_info" type.Gravatar Matej Kosik2015-12-18
* | COMMENTS: added to some variants of the "Constr.kind_of_term" type.Gravatar Matej Kosik2015-12-18
* | COMMENTS: added to the "Names" module.Gravatar Matej Kosik2015-12-18
* | ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convGravatar Matej Kosik2015-12-17
* | ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | Fixing e3cefca41b about supposingly simplifying primitive projectionsGravatar Hugo Herbelin2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * bug fixes to vm computation + test cases.Gravatar Gregory Malecha2015-12-09