aboutsummaryrefslogtreecommitdiff
path: root/checker/mod_checking.ml
AgeCommit message (Expand)Author
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-23coqchk: Cleanup environment manipulation in check_constant_declarationGaëtan Gilbert
2019-08-16Fix typing_flags in the checkerSimonBoulier
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
2019-05-30Merge PR #10269: Checker: don't use monomorphic universes attached to a constantPierre-Marie Pédrot
2019-05-29Merge PR #10252: Various dynamic assertions and cleanups in opaque typingMaxime Dénès
2019-05-28Same universe constraint fix for the checker.Pierre-Marie Pédrot
2019-05-28Checker: don't use monomorphic universes attached to a constantGaëtan Gilbert
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-24Move body_of_constant_body to Global and specialize its uses.Pierre-Marie Pédrot
2019-05-06Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.Hugo Herbelin
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23Fix #8937: inductive conversion in coqchk subtypingGaëtan Gilbert
2018-11-06Checker now disables VM and nativeMaxime Dénès
2018-11-06[checker] Check univ constraints induced by module subtypingMaxime Dénès
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-06-21Remove enforce_leq from checkerGaëtan Gilbert
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-09-21Fix -silent flag of coqchk after ff918e4.Maxime Dénès
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
2015-10-02Univs: update checkerMatthieu Sozeau
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2014-12-26coqchk: flush the pp buffer from time to timeEnrico Tassi
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-06Fix checking of constants in checker. Prelude can now be checked.Matthieu Sozeau
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26checker and votour ported to new vo format (after -vi2vo)Enrico Tassi
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:06:35 +0000