index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
/
values.ml
Commit message (
Expand
)
Author
Age
*
Remove Sorts.contents
Gaëtan Gilbert
2018-06-26
*
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-23
*
Change the proj_ind field from MutInd.t to inductive.
Pierre-Marie Pédrot
2018-06-23
*
Merge PR #7841: Remove Canary
Pierre-Marie Pédrot
2018-06-19
|
\
|
*
Remove Canary.
whitequark
2018-06-18
*
|
Remove the proj_body field from the kernel.
Pierre-Marie Pédrot
2018-06-17
*
|
Remove the proj_eta field of the kernel.
Pierre-Marie Pédrot
2018-06-17
*
|
Getting rid of the const_proj field in the kernel.
Pierre-Marie Pédrot
2018-06-17
|
/
*
Fix the checker by merely adapting the data structure.
Pierre-Marie Pédrot
2018-06-07
*
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-28
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-02-16
*
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
*
Store the conversion oracle in constant and inductive definitions.
Pierre-Marie Pédrot
2018-01-14
*
Add interfaces for checker and remove dead code.
Maxime Dénès
2018-01-10
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Merge PR #955: Do not hashcons universes beforehand
Maxime Dénès
2017-09-15
|
\
|
*
Do not hashcons universes beforehand.
Pierre-Marie Pédrot
2017-09-01
*
|
Statically enforcing that module types have no retroknowledge.
Pierre-Marie Pédrot
2017-08-29
*
|
Separating the module_type and module_body types by using a type parameter.
Pierre-Marie Pédrot
2017-08-29
|
/
*
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A short cleanup
Amin Timany
2017-06-16
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Correct coqchk reduction
Amin Timany
2017-06-16
*
Fixing the checker.
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
|
\
|
*
Fixing the checker.
Pierre-Marie Pédrot
2016-06-16
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
Update cic.mli MD5 after header update.
Maxime Dénès
2016-01-20
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Univs: update checker
Matthieu Sozeau
2015-10-02
*
|
Updating checksum in checker (9c732a5cc continued).
Hugo Herbelin
2015-07-12
*
|
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
|
Checker: Fix bug #4282
Matthieu Sozeau
2015-07-07
|
*
Adjust checker after `Assume [Positive]`.
Arnaud Spiwack
2015-06-25
|
/
*
Splitting the library representation on disk in two.
Pierre-Marie Pédrot
2015-06-24
*
Exporting memory representation of STM tasks for votour.
Pierre-Marie Pédrot
2015-03-25
*
Fixing representation of dynamics in votour (again).
Pierre-Marie Pédrot
2015-03-24
*
Fix checker after addition of a universe context in with t := c constraints.
Matthieu Sozeau
2015-02-26
*
Update hash of cic.mli in checker/values.ml,
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
Vi2vo: fix handling of univ constraints coming from the body
Enrico Tassi
2014-12-23
*
Fixing checker representation of values.
Pierre-Marie Pédrot
2014-12-19
*
update md5 sums to make "make check" work
Enrico Tassi
2014-12-19
*
Fixing checker representation of universe lists.
Pierre-Marie Pédrot
2014-12-18
[next]