aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
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
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-06-28Reify libobject containersMaxime Dénès
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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-04Remove the discharge segment from vo files.Pierre-Marie Pédrot
2019-06-04Slightly tweak the representation of dischargeable opaque proofs.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-28Merge PR #10258: Remove the delayed universe table from object files.Enrico Tassi
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-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
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-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-05-21Fixing typos - Part 1JPR
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:58:15 +0000