aboutsummaryrefslogtreecommitdiff
path: root/checker/term.mli
AgeCommit message (Expand)Author
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-06-16Correct coqchk reductionAmin Timany
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-02-15CLEANUP: Simplifying the changes done in "checker/*"Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2014-09-05Remove unused substitution functions in checker.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of subst_un...Matthieu Sozeau
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-04-15Checker: get rid of code handling section variablesletouzey
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
2013-02-12Checker: re-sync vo structures after Maxime's commit 16136letouzey
2012-12-14Modulification of identifierppedrot
2010-09-24Checker: remove some dead codeletouzey
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2009-03-02porting r11900 11905 and 11953 to trunkbarras
2008-05-22fixed dependency problems with the checkerbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:39:44 +0000