aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-11-09Merge PR #11017: Make [Proof_global.closed_proof_output] opaquePierre-Marie Pédrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
2019-11-08Merge PR #11069: Do not include final stops in queries. (Fixes #11058)Pierre-Marie Pédrot
2019-11-08coqdep: only output vos when passed -vosGaëtan Gilbert
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
2019-11-08Merge PR #11042: The "univ poly can capture global univs" checker side bug is...Théo Zimmermann
2019-11-07Do not rely on the user settings but on the actual window size. (Fixes #10956)Guillaume Melquiond
2019-11-07Do not include final stops in queries. (Fixes #11058)Guillaume Melquiond
2019-11-07The "univ poly can capture global univs" checker side bug is fixedGaëtan Gilbert
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ...Pierre-Marie Pédrot
2019-11-07Merge PR #11059: Swap parsing precedence of `::` and `,` ; Fix #10116Pierre-Marie Pédrot
2019-11-06Merge PR #11038: fix(*.opam): Add missing version "dev"Emilio Jesus Gallego Arias
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-06Merge PR #11041: Cite POPL19 SProp paperThéo Zimmermann
2019-11-06Merge PR #11051: elpi 1.8Gaëtan Gilbert
2019-11-05Fixing test-suiteKenji Maillard
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
2019-11-05overlayEnrico Tassi
2019-11-05elpi 1.8Enrico Tassi
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
2019-11-04Prevent redefinition of Ltac2 types; fix #10097Kenji Maillard
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
2019-11-04fix(*.opam): Add missing versionErik Martin-Dorel
2019-11-03Merge PR #10958: Elan → Stratego in documentation of `rewrite_strat`.Théo Zimmermann
2019-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
2019-11-02Merge PR #11007: [classes] Some refactoring on proof save preparation.Gaëtan Gilbert
2019-11-01Merge PR #11028: Update the deprecation doc of `Shrink Obligations`Clément Pit-Claudel
2019-11-01Merge PR #10647: Expose universe processing in comInductive.Gaëtan Gilbert
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01minor cleanup of anonymous functionsGaëtan Gilbert
2019-11-01Expose universe processing in comInductive.Jan-Oliver Kaiser
2019-11-01Merge PR #8642: Compiled interfaces with -vos and -vok optionsPierre-Marie Pédrot
2019-11-01Merge PR #11019: enforcing Ltac2 constructor name are uppercasedPierre-Marie Pédrot
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-11-01enforcing Ltac2 cosntructors name are uppercase in open typesKenji Maillard
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01Teach coq_dune about the empty .vos produced by coqcGaëtan Gilbert
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01[make] install .vos along with .voEnrico Tassi
2019-11-01fix installation of vos files in coq Makefilecharguer
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall th...charguer
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01Changelog entryMaxime Dénès
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:18:13 +0000