aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
* | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
* Merge PR #783: Remove some useless code in Term_typingGravatar Maxime Dénès2017-07-17
|\
* | The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
* | Adding a comment regarding De Bruijn universe indices in the kernel.Gravatar Pierre-Marie Pédrot2017-07-12
* | Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* | Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* | Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* | Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
* | Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* | Asserting that monomorphic section variables have no abstracted context.Gravatar Pierre-Marie Pédrot2017-07-11
* | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* | Removing a redundant universe instance information in native compute.Gravatar Pierre-Marie Pédrot2017-07-10
* | Merge PR #853: Clean 'with Definition' implementation.Gravatar Maxime Dénès2017-07-06
|\ \
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * | Removing dead code in Subtyping.Gravatar Pierre-Marie Pédrot2017-07-04
| * | Removing a few suspicious functions from the kernel.Gravatar Pierre-Marie Pédrot2017-07-03
| * | Do not add original constraints to the environment in 'with Definition' check.Gravatar Pierre-Marie Pédrot2017-07-03
|/ /
* | 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
|\ \ \
| | | * Remove some useless code in Term_typingGravatar Gaëtan Gilbert2017-06-13
| |_|/ |/| |
* | | 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