aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/cic.mli
Commit message (Expand)AuthorAge
* Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A short cleanupGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Correct coqchk reductionGravatar Amin Timany2017-06-16
* Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-16
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* | Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
| * Adjust checker after `Assume [Positive]`.Gravatar Arnaud Spiwack2015-06-25
|/
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Checker: vo validation checks the absence of Var/Evar/MetaGravatar letouzey2013-04-15
* Checker: vo validation is now done in check.ml (and always)Gravatar letouzey2013-04-15
* Checker: empty sections hardcoded in cb and mindGravatar letouzey2013-04-15
* Checker: reified encoding of .vo types in values.mlGravatar letouzey2013-04-15
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 19:50:22 +0000