aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
AgeCommit message (Expand)Author
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-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-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
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-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-28Merge PR #10258: Remove the delayed universe table from object files.Enrico Tassi
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-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-21More informative error on vo validation failureGaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-26Merge PR #8102: Fix #8043: Unsafe assignment in checker.Maxime Dénès
2018-09-07Canonical representation of kernel substitutions.Pierre-Marie Pédrot
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-20Fix #8043: Unsafe assignment in checker.Pierre-Marie Pédrot
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-18Remove Canary.whitequark
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:31:38 +0000