aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2020-08-19[coqchk] Look inside inner modules as wellJason Gross
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-05-22[coqchk] Improve previous heuristic.Pierre Roux
2020-05-22[coqchk] Fix #5030Pierre Roux
2020-05-22[coqchk] Change list to setPierre Roux
2020-05-13Centralize the OCaml version-checking function.Pierre-Marie Pédrot
2020-05-13Store the OCaml version used for Coq in vo files.Pierre-Marie Pédrot
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-26Open object files in binary mode.Pierre-Marie Pédrot
2020-04-26Move the ObjFile module to its own file.Pierre-Marie Pédrot
2020-04-26Implement a name-based representation for vo files.Pierre-Marie Pédrot
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-16Checker: factorize handling of typing flagsGaëtan Gilbert
2020-04-13always debug validate failuresGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-11Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (#11624)Pierre Roux
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-03-08Template polymorphism is now a property of the inductive block.Pierre-Marie Pédrot
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-02-05Remove a dubious part of the checker code relying on a universe contextPierre-Marie Pédrot
2020-02-05Store the template polymorphic context inside the TemplateArity node.Pierre-Marie Pédrot
2020-01-27Checker: use inductive's check_template flagGaëtan Gilbert
2020-01-20Merge PR #11411: Checker validation now performed over reified dataGaëtan Gilbert
2020-01-16Move the per-architecture check of marshalled Uint63s to Values.Pierre-Marie Pédrot
2020-01-16Checker validation acts on object representations rather than objects.Pierre-Marie Pédrot
2020-01-16Code factorization in checker validation.Pierre-Marie Pédrot
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
2019-12-19Merge PR #11247: Use standard float and integer datatypes in Votour represent...Maxime Dénès
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-12-09dune: Add byte mode for coqchk and coqide (fix dune-dbg for dune 2)Gaëtan Gilbert
2019-12-06Use standard float an integer datatypes in Votour representation.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Add primitive floats to checkerPierre Roux
2019-10-18Fix votour after the change of representation of opaques.Pierre-Marie Pédrot
2019-10-04Merge Direct and Indirect nodes in Opaqueproof.Pierre-Marie Pédrot
2019-09-16Optimize multiple importsMaxime Dénès
2019-09-16Specialize `ImportObject` to `Export`Maxime Dénès
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-23coqchk: Cleanup environment manipulation in check_constant_declarationGaëtan Gilbert
2019-08-16Fix typing_flags in the checkerSimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:47:04 +0000