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
*
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
|
\
\
*
\
\
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
|
*
|
|
A few typos.
Hugo Herbelin
2017-06-04
|
|
/
/
*
/
/
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
/
/
*
|
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
*
|
Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.
Maxime Dénès
2017-05-29
|
\
\
*
|
|
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
|
Merge PR#646: Revised behavior on ill-formed identifiers
Maxime Dénès
2017-05-23
|
\
\
\
*
\
\
\
Merge PR#518: Faster universe unification
Maxime Dénès
2017-05-23
|
\
\
\
\
|
|
*
|
|
Revised behavior on ill-formed identifiers.
Hugo Herbelin
2017-05-20
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR#572: Replacing costly merges in UGraph.
Maxime Dénès
2017-05-11
|
\
\
\
\
*
\
\
\
\
Merge PR#602: Fix more warnings
Maxime Dénès
2017-05-03
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
|
|
*
|
|
|
|
Remove dead code in native compiler.
Maxime Dénès
2017-05-02
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-02
|
\
\
\
\
\
\
*
|
|
|
|
|
|
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
*
|
|
|
|
|
|
Fix for bug 5507. Mispelt de Bruijn.
Théo Zimmermann
2017-05-01
*
|
|
|
|
|
|
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-28
|
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
|
|
*
|
|
|
|
|
Remove some unused values and types
Gaetan Gilbert
2017-04-27
|
|
*
|
|
|
|
|
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
|
|
*
|
|
|
|
|
Locally disable some warnings.
Gaetan Gilbert
2017-04-27
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
Fast path when checking equality of universe levels in UState.
Pierre-Marie Pédrot
2017-04-27
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
COMMENT: Pre_env.env
Matej Kosik
2017-04-20
*
|
|
|
|
|
correcting a typo in a comment
Matej Kosik
2017-04-20
*
|
|
|
|
|
correcting comments in the "Context" module
Matej Kosik
2017-04-20
*
|
|
|
|
|
simplifying "Environ.push_named" function
Matej Kosik
2017-04-20
*
|
|
|
|
|
refactoring "Names.DirPath.is_empty" function
Matej Kosik
2017-04-20
*
|
|
|
|
|
refactoring "Names.DirPath.compare" function
Matej Kosik
2017-04-20
*
|
|
|
|
|
refactoring "Names.DirPath.equal" function
Matej Kosik
2017-04-20
|
|
|
*
|
|
Replacing costly merges in UGraph.
Pierre-Marie Pédrot
2017-04-18
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
\
\
\
\
[next]
Amin Timany
Maxime Dénès
Matej Košík
Emilio Jesus Gallego Arias
Thomas Sibut-Pinote
Hugo Herbelin
Jason Gross
Théo Zimmermann
Gaetan Gilbert
Pierre-Marie Pédrot