aboutsummaryrefslogtreecommitdiff
path: root/checker/indtypes.ml
AgeCommit message (Expand)Author
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-10-31Fix #8873: coqchk on inductive with letin parameterGaëtan Gilbert
2018-10-09[coqchk] Fix checking of inductive typesVincent Laporte
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-07-03checker Indtypes: remove unused argumentsGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-01-25[checker] Better error message for bad recursive treesMaxime Dénès
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Properly instantiate contexts before pushingAmin Timany
2017-06-16Enable the checking of ind subtyping in checkerAmin Timany
2017-06-16Correct coqchk checking subtyping relation for inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-28Fix a bug in checkerAmin Timany
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-02-15CLEANUP: Simplifying the changes done in "checker/*"Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-09-03Implementing Herbelin's fix for the "NonPar" bugmlasson
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-03-02Now accepting unit props in mutual definitionsBruno Barras
2015-01-12Update headers.Maxime Dénès
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-07Removing 'open Univ' from checker.Pierre-Marie Pédrot
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-03-18Fixing checker with respect to new kernel name structure and hashmaps.Pierre-Marie Pédrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Rtree : cleanup of the comparing codeletouzey
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-02-19Dir_path --> DirPathletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of mod_bound_idppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:34:42 +0000