index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
...
*
|
More precise type for universe entries.
Pierre-Marie Pédrot
2017-07-26
|
/
*
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-25
*
[api] Put modules in order in API.{mli,ml}
Emilio Jesus Gallego Arias
2017-07-25
*
Merge PR #783: Remove some useless code in Term_typing
Maxime Dénès
2017-07-17
|
\
*
|
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-13
*
|
Adding a comment regarding De Bruijn universe indices in the kernel.
Pierre-Marie Pédrot
2017-07-12
*
|
Moving the last bits of abtraction-breaking code out of the kernel.
Pierre-Marie Pédrot
2017-07-11
*
|
Fix nonsensical universe abstraction in the kernel.
Pierre-Marie Pédrot
2017-07-11
*
|
Properly handling polymorphic inductive subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
*
|
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
*
|
Safe API for accessing universe constraints of global references.
Pierre-Marie Pédrot
2017-07-11
*
|
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
*
|
Asserting that monomorphic section variables have no abstracted context.
Pierre-Marie Pédrot
2017-07-11
*
|
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
*
|
Removing a redundant universe instance information in native compute.
Pierre-Marie Pédrot
2017-07-10
*
|
Merge PR #853: Clean 'with Definition' implementation.
Maxime Dénès
2017-07-06
|
\
\
*
|
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
|
Removing dead code in Subtyping.
Pierre-Marie Pédrot
2017-07-04
|
*
|
Removing a few suspicious functions from the kernel.
Pierre-Marie Pédrot
2017-07-03
|
*
|
Do not add original constraints to the environment in 'with Definition' check.
Pierre-Marie Pédrot
2017-07-03
|
/
/
*
|
Fix a bug in cumulativity
Amin Timany
2017-06-16
*
|
A short cleanup
Amin Timany
2017-06-16
*
|
use map_constr more efficiently
Amin Timany
2017-06-16
*
|
Optimization
Amin Timany
2017-06-16
*
|
Use a smart map_constr
Amin Timany
2017-06-16
*
|
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
|
Move univops from kernel to library
Amin Timany
2017-06-16
*
|
Simplify Univ.ml
Amin Timany
2017-06-16
*
|
Disable debug printing
Amin Timany
2017-06-16
*
|
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
*
|
Fix bugs
Amin Timany
2017-06-16
*
|
Squashed commit of the following:
Amin Timany
2017-06-16
*
|
Fix cum/conv for inductive types
Amin Timany
2017-06-16
*
|
Use inductive subtyping for conv/cumul
Amin Timany
2017-06-16
*
|
Add subtyping inference for inductive types
Amin Timany
2017-06-16
*
|
Correct subtyping check for constructors
Amin Timany
2017-06-16
*
|
Fix typo in error message
Amin Timany
2017-06-16
*
|
Check subtyping of inductive types in Kernel
Amin Timany
2017-06-16
*
|
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
*
|
New datastructure for universes of inductive types
Amin Timany
2017-06-16
*
|
Extend definition of inductives to include subtyping info
Amin Timany
2017-06-16
*
|
Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613
Maxime Dénès
2017-06-14
|
\
\
*
\
\
Merge PR#448: Do not recompute twice the whnf of terms in conversion.
Maxime Dénès
2017-06-14
|
\
\
\
|
|
|
*
Remove some useless code in Term_typing
Gaëtan Gilbert
2017-06-13
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR#714: Print feature Proof-of-Concept (episode 2)
Maxime Dénès
2017-06-13
|
\
\
\
*
|
|
|
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
|
|
|
*
[kernel] Improve proof using message, fixes bugzilla #3613
Emilio Jesus Gallego Arias
2017-06-07
*
|
|
|
Put all plugins behind an "API".
Matej Kosik
2017-06-07
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR#728: A few typos.
Maxime Dénès
2017-06-06
|
\
\
\
|
|
*
|
Added support for a side effect on constants in reduction functions.
Thomas Sibut-Pinote
2017-06-04
[prev]
[next]