index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
/
cic.mli
Commit message (
Expand
)
Author
Age
*
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
*
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
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Fix checker to handle projections with eta and universe polymorphism correctly.
Matthieu Sozeau
2014-09-06
*
Fix checker treatment of inductives using subst_instances instead of subst_un...
Matthieu Sozeau
2014-09-05
*
Rename eta_expand_ind_stacks, fix the one from the checker and adapt
Matthieu Sozeau
2014-09-05
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Adapt the checker to polymorphic universes and projections (untested).
Matthieu Sozeau
2014-05-08
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
Hugo Herbelin
2014-04-28
*
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
*
Slightly more compact representation of 'a substituted type,
ppedrot
2013-09-14
*
Change in vo format : digest aren't Marshalled anymore
letouzey
2013-08-22
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Checker: vo validation checks the absence of Var/Evar/Meta
letouzey
2013-04-15
*
Checker: vo validation is now done in check.ml (and always)
letouzey
2013-04-15
*
Checker: empty sections hardcoded in cb and mind
letouzey
2013-04-15
*
Checker: reified encoding of .vo types in values.ml
letouzey
2013-04-15
*
Checker: regroup all vo-related types in cic.mli
letouzey
2013-04-15