aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Avoiding a variable shadowing in the kernel.Gravatar Pierre-Marie Pédrot2017-07-26
* Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Remove a horrendous hack in Declare to retrieve exported side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
* 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
|\ \ \