aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* A short cleanupGravatar Amin Timany2017-06-16
* use map_constr more efficientlyGravatar Amin Timany2017-06-16
* OptimizationGravatar Amin Timany2017-06-16
* Use a smart map_constrGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Move univops from kernel to libraryGravatar Amin Timany2017-06-16
* Simplify Univ.mlGravatar Amin Timany2017-06-16
* Disable debug printingGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Fix bugsGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Fix cum/conv for inductive typesGravatar Amin Timany2017-06-16
* Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
* Add subtyping inference for inductive typesGravatar Amin Timany2017-06-16
* Correct subtyping check for constructorsGravatar Amin Timany2017-06-16
* Fix typo in error messageGravatar Amin Timany2017-06-16
* Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613Gravatar Maxime Dénès2017-06-14
|\
* \ Merge PR#448: Do not recompute twice the whnf of terms in conversion.Gravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \
* | | | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| | | * [kernel] Improve proof using message, fixes bugzilla #3613Gravatar Emilio Jesus Gallego Arias2017-06-07
* | | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
| |_|/ |/| |
* | | Merge PR#728: A few typos.Gravatar Maxime Dénès2017-06-06
|\ \ \
| | * | Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
| * | | A few typos.Gravatar Hugo Herbelin2017-06-04
| |/ /
* / / Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/ /
* | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* | Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.Gravatar Maxime Dénès2017-05-29
|\ \
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | Merge PR#646: Revised behavior on ill-formed identifiersGravatar Maxime Dénès2017-05-23
|\ \ \
* \ \ \ Merge PR#518: Faster universe unificationGravatar Maxime Dénès2017-05-23
|\ \ \ \
| | * | | Revised behavior on ill-formed identifiers.Gravatar Hugo Herbelin2017-05-20
| |/ / / |/| | |
* | | | Merge PR#572: Replacing costly merges in UGraph.Gravatar Maxime Dénès2017-05-11
|\ \ \ \
* \ \ \ \ Merge PR#602: Fix more warningsGravatar Maxime Dénès2017-05-03
|\ \ \ \ \
* \ \ \ \ \ Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \
| | * | | | | Remove dead code in native compiler.Gravatar Maxime Dénès2017-05-02
| |/ / / / / |/| | | | |
* | | | | | Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \
* | | | | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | | | | | | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | | | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \ \ \ \ \ \
| | * | | | | | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | * | | | | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | * | | | | | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | * | | | | | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
| |/ / / / / / |/| | | | | |
| | | | * | | Fast path when checking equality of universe levels in UState.Gravatar Pierre-Marie Pédrot2017-04-27
| |_|_|/ / / |/| | | | |