aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-11-12Merge PR #11067: Expand documentation about generating a Docker image.Emilio Jesus Gallego Arias
2019-11-12Expand documentation about generating a Docker image.Pierre-Marie Pédrot
2019-11-12Merge PR #11092: [dune] Have only one rule calling configureEmilio Jesus Gallego Arias
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
2019-11-11Have only one dune rule calling configurePierre Roux
2019-11-11Do not export the internals of the prepare_hint function.Pierre-Marie Pédrot
2019-11-11Merge PR #11032: Run update-compat script with --release option.Pierre-Marie Pédrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 16:38:04 +0000