aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-16Get rid of the compilation date from the binaries to make them more stable.Guillaume Melquiond
2021-01-07Merge PR #13718: Move printing and sorting out of AcyclicGraphcoqbot-app[bot]
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:34:51 +0000