aboutsummaryrefslogtreecommitdiff
path: root/checker/cic.mli
AgeCommit message (Expand)Author
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Fixing the checker.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Univs: update checkerMatthieu Sozeau
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
2015-06-25Adjust checker after `Assume [Positive]`.Arnaud Spiwack
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-02-26Fix checker after addition of a universe context in with t := c constraints.Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-06rename: vi -> vioEnrico Tassi
2014-12-17checker: Change in library on disk values, now using context_sets instead ofMatthieu Sozeau
2014-12-17Update checker/values and cic due to changes in case_info and record_body.Matthieu Sozeau
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of subst_un...Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-02-26checker and votour ported to new vo format (after -vi2vo)Enrico Tassi
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-08State Transaction Machinegareuselesinge
2013-04-15Checker: vo validation checks the absence of Var/Evar/Metaletouzey
2013-04-15Checker: vo validation is now done in check.ml (and always)letouzey
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
2013-04-15Checker: reified encoding of .vo types in values.mlletouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 15:27:33 +0000