aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
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
2019-05-06Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.Hugo Herbelin
2019-04-02coqchk: use unsafe marshal for dependencies of -norec librariesGaëtan Gilbert
2019-04-02coqchk: don't marshal opaques for dependencies of -norec librariesGaëtan Gilbert
2019-04-02coqchk: do not validate dependencies of -norec librariesGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Merge PR #9700: [dune] [checker] Don't install internal checker library.Théo Zimmermann
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-05[dune] [checker] Don't install internal checker library.Emilio Jesus Gallego Arias
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-25Merge PR #9511: Enable whitespace checking for some forgotten files.Théo Zimmermann
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-21Fix #9613 use -coqlib when invoking coqchkGaëtan Gilbert
2019-02-20Enable whitespace checking for some forgotten files.Gaëtan Gilbert
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:59:46 +0000