aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
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
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-10[checker] avoid some printing in non verbose modeEnrico Tassi
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:04:11 +0000