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
*
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
*
checker: Change in library on disk values, now using context_sets instead of
Matthieu Sozeau
2014-12-17
*
Update checker/values and cic due to changes in case_info and record_body.
Matthieu Sozeau
2014-12-17
*
Fix checker/values.ml with latest changes due to projections and universes.
Matthieu Sozeau
2014-09-05
*
Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately
Hugo Herbelin
2014-04-29
*
Fixing checker with respect to new kernel name structure and hashmaps.
Pierre-Marie Pédrot
2014-03-18
*
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-11
*
checker and votour ported to new vo format (after -vi2vo)
Enrico Tassi
2014-02-26
*
votour: better error messages
Enrico Tassi
2014-02-26
*
fix checker w.r.t. mutual_inductive_body and constant_body
Enrico Tassi
2014-02-26
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
Slightly more compact representation of 'a substituted type,
ppedrot
2013-09-14
*
Adding dynamic value printing to votour through a registering mechanism.
ppedrot
2013-08-23
*
Change in vo format : digest aren't Marshalled anymore
letouzey
2013-08-22
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Repair coqcheck : constant_body constraints are also future
letouzey
2013-08-20
*
checker validation fixed w.r.t. Futures
gareuselesinge
2013-08-09
[next]