aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-13Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move extensi...Pierre-Marie Pédrot
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-11-13[configure] Remove grammar and dev from core_src_dirs.Emilio Jesus Gallego Arias
2018-11-13Merge PR #8978: nix helpers for debugging external projects from CIEmilio Jesus Gallego Arias
2018-11-13Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.Pierre-Marie Pédrot
2018-11-12Merge PR #8979: Skip submodules in HoTT CI script.Emilio Jesus Gallego Arias
2018-11-12Merge PR #8960: [dune] Build `cmxs` files instead of `cmxa` in "quick" target.Enrico Tassi
2018-11-12Skip submodules in HoTT CI script.Gaëtan Gilbert
2018-11-12Merge PR #8962: [ci] Add paramcoq to CI.Gaëtan Gilbert
2018-11-12Merge PR #8892: Fix part of #8224: grounding open term in fixpointsPierre-Marie Pédrot
2018-11-12Merge PR #8972: Fix #4771: Substitution of inline global reference in tactics...Pierre-Marie Pédrot
2018-11-12Set codeowners for dev/ci/nixVincent Laporte
2018-11-12Helpers for debugging external projects from CIVincent Laporte
2018-11-12Merge PR #8938: [Plugins] Remove some dead codePierre-Marie Pédrot
2018-11-12Merge PR #8958: [clib] Remove unneeded `get_extension` function.Pierre-Marie Pédrot
2018-11-12Test case for #4771: Substitution of inline global reference in tactics is br...Maxime Dénès
2018-11-12Fix #4771: Substitution of inline global reference in tactics is brokenMaxime Dénès
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-12[clib] Remove unneeded `get_extension` function.Emilio Jesus Gallego Arias
2018-11-11Merge PR #8795: Encapsulating declarations of primitive string syntax in a mo...Jason Gross
2018-11-10[ci] Add paramcoq to CI.Emilio Jesus Gallego Arias
2018-11-09Merge PR #8949: Remove checker printersEmilio Jesus Gallego Arias
2018-11-09Merge PR #8956: Fix dune runtest invocationEmilio Jesus Gallego Arias
2018-11-09[dune] Build `cmxs` files instead of `cmxa` in "quick" target.Emilio Jesus Gallego Arias
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Merge PR #8820: Standardize handling of Automatic Introduction.Pierre-Marie Pédrot
2018-11-09Merge PR #8408: [doc] [ssr] Fix renderingThéo Zimmermann
2018-11-09Fix dune runtest invocationGaëtan Gilbert
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-09Adding an overlay for #8601.Pierre-Marie Pédrot
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Remove remnants of polymorphic instance name registration.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-11-09Merge PR #8947: Ensure termination of `file_exists_respecting_case`Emilio Jesus Gallego Arias
2018-11-08Remove checker printersGaëtan Gilbert
2018-11-08Merge PR #8944: Revert PR #8923 (require camlp5 >=7.06)Gaëtan Gilbert
2018-11-08Ensure termination of `file_exists_respecting_case`Vincent Laporte
2018-11-08Merge PR #8098: Update/improve two aspects of the merging process.Maxime Dénès
2018-11-08Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."Pierre-Marie Pédrot
2018-11-07Merge PR #8923: Bump camlp5 minimal version and use its safe API.Emilio Jesus Gallego Arias
2018-11-07Merge PR #8934: Revert "Do not allow spliting in res_pf, this is reserved for...Matthieu Sozeau
2018-11-07Merge PR #8928: Fixes #8910: typo in nameops.mlPierre-Marie Pédrot
2018-11-07[Funind plugin] Remove some dead codeVincent Laporte
2018-11-07[Firstorder plugin] Remove some dead codeVincent Laporte
2018-11-07[CC plugin] Remove dead codeVincent Laporte
2018-11-07[R syntax plugin] Remove some dead codeVincent Laporte
2018-11-07Merge PR #8901: [dune] Add "quick" and "check" targets for fast builds.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 19:26:01 +0000