aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
| | | | | | * | Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-12
| |_|_|_|_|/ / |/| | | | | |
| | | * | | | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
| | | * | | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | * dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Gaëtan Gilbert2018-02-11
| |_|_|_|_|/ |/| | | | |
| | | * | | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | * | | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
| | | * | | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| | | * | | Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
| |_|/ / / |/| | | |
| | | | * [nit] Remove some unnecessary global `open Feedback`Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | |/ | | |/|
| | * | [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| |/ / |/| |
* | | Merge PR #6685: Use whd-all on rigid-flex conversion.Gravatar Maxime Dénès2018-02-07
|\ \ \
* \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \
| | * | | Respect the transparent state of the current conversion on strong weak-head.Gravatar Pierre-Marie Pédrot2018-02-05
* | | | | [native_compute] Fix handling of evars in conversionGravatar Maxime Dénès2018-02-05
* | | | | [native_compute] Remove useless conversion to list in reification.Gravatar Maxime Dénès2018-02-05
| | | * | Delay computation of lifts in the reduction machine.Gravatar Pierre-Marie Pédrot2018-02-04
| |_|/ / |/| | |
| * | | CClosure.unfold_projection: don't catch Not_found, assume env is okGravatar Gaëtan Gilbert2018-02-02
| * | | kernel: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
|/ / /
| * / Use whd-all on rigid-flex conversion.Gravatar Pierre-Marie Pédrot2018-02-02
|/ /
* | Merge PR #6666: Fix reduction of primitive projections on coinductive records...Gravatar Maxime Dénès2018-01-30
|\ \
* \ \ Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-30
|\ \ \
| | * | [native_compute] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
* | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
| |/ / |/| |
| * | Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-24
|/ /
* | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Gravatar Maxime Dénès2018-01-23
|\ \
* \ \ Merge PR #6506: Fast rel lookupGravatar Maxime Dénès2018-01-22
|\ \ \
| | * | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
| |/ / |/| |
* | | Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
* | | Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionGravatar Maxime Dénès2018-01-13
|\ \ \
* | | | Enforce that polymorphic definitions do not generate internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| * | | Remove references to removed Unicode.UnsupportedGravatar Jasper Hugunin2018-01-11
|/ / /
* | | Add a comment about universe lifting in sections in the kernel.Gravatar Pierre-Marie Pédrot2017-12-31
* | | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
* | | Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* | | Hardening universe abstraction in Cooking.Gravatar Pierre-Marie Pédrot2017-12-30
| * | Share the rel environment between Environ.env and reduction cache.Gravatar Pierre-Marie Pédrot2017-12-29
| * | Fast environment lookup for rels.Gravatar Pierre-Marie Pédrot2017-12-29
|/ /
* | [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* | Merge PR #6469: No universe constraints in Let definitionsGravatar Maxime Dénès2017-12-22
|\ \
* \ \ Merge PR #6449: Let definitions must not contain side-effects when reaching t...Gravatar Maxime Dénès2017-12-20
|\ \ \
| | * | Let definitions do not create new universe constraints.Gravatar Pierre-Marie Pédrot2017-12-19
| | * | Specific type for section definition entries.Gravatar Pierre-Marie Pédrot2017-12-19
| |/ /
* | | Fix order of let-in representation comment.Gravatar Jasper Hugunin2017-12-19
| * | Let definitions must not contain side-effects when reaching the kernel.Gravatar Pierre-Marie Pédrot2017-12-16
|/ /
* | Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\ \
| | * Cosmetic: using "types" rather "constr" in some types of term.mli.Gravatar Hugo Herbelin2017-12-14
| | * Fixing a bug of Print for inductive types with let-ins in parameters.Gravatar Hugo Herbelin2017-12-14
| | * Fixes incorrect anomaly message in lambda/prod_applist_assum + typo in doc.Gravatar Hugo Herbelin2017-12-14
* | | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ | |_|/ |/| |
* | | Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 13:13:29 +0000