index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
indtypes.ml
Commit message (
Expand
)
Author
Age
*
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Clean up universes of constants and inductives
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
*
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
*
Extend definition of inductives to include subtyping info
Amin Timany
2017-06-16
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Introducing contexts parameterized by the inner term type.
Pierre-Marie Pédrot
2017-02-14
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
Adding a local type-in-type flag in kernel declarations.
Pierre-Marie Pédrot
2016-06-18
*
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
*
|
This is an attempt to clarify terminology in choosing variable names
Hugo Herbelin
2016-04-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
\
|
*
|
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
|
*
|
Fixing bde12b70 about reporting ill-formed constructor.
Hugo Herbelin
2016-01-26
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Fixing e3cefca41b about supposingly simplifying primitive projections
Hugo Herbelin
2015-12-15
*
|
|
Slight simplification of the code of primitive projection (in relation
Hugo Herbelin
2015-12-05
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
|
*
|
Fixing fix c71aa6b to primitive projections.
Hugo Herbelin
2015-11-18
|
*
|
Slightly documenting code for building primitive projections.
Hugo Herbelin
2015-11-18
|
*
|
Fixing logical bugs in the presence of let-ins in computiong primitive
Hugo Herbelin
2015-11-18
*
|
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
|
*
|
Dead code from the commit having introduced primitive projections (a4043608).
Hugo Herbelin
2015-11-10
|
*
|
Fixing a bug in reporting ill-formed constructor.
Hugo Herbelin
2015-11-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
|
*
|
Fixing a bug in reporting ill-formed inductive.
Hugo Herbelin
2015-10-22
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
|
*
|
Univs: inductives, remove unneeded test
Matthieu Sozeau
2015-10-14
*
|
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
|
*
|
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-06
|
\
|
|
|
*
|
Implementing Herbelin's fix for the "NonPar" bug
mlasson
2015-09-03
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
|
\
|
|
|
*
|
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
|
*
|
Kernel: primitive projections handling of let-ins
Matthieu Sozeau
2015-07-09
|
*
|
Template polymorphism: A bug-fix for Bug #4258
mlasson
2015-07-09
|
|
*
Add a corresponding field in `mutual_inductive_entry` (part 2).
Arnaud Spiwack
2015-06-24
[next]