aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-12Automatically generate names for universes.Gaëtan Gilbert
2018-11-12Do not qualify universe names by section path.Gaëtan Gilbert
2018-11-12Fix incorrect coq-prog-args in unideclsGaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
2018-11-12Only declare univ binders once for mutindGaë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-12CoqHammer CILukasz Czajka
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-11CoqIDE: pass the parent window to all methods liable to open a question box.Hugo Herbelin
2018-11-11A private copy of lablgtk's question_box supporting the "parent" option.Hugo Herbelin
2018-11-11CoqIDE: ensure that the configuration box is not hidden by the main window.Hugo Herbelin
2018-11-11CoqIDE: remove obselete menu item "Complete word".Hugo Herbelin
2018-11-11CoqIDE: Do not rebind up and down in microPG mode.Hugo Herbelin
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 pull request #19 from SkySkimmer/gitignoreEmilio Jesús 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-09[dune] [ide] Install data files.Emilio Jesus Gallego Arias
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Add .cmt and generated ml files to gitignoreGaëtan Gilbert
2018-11-09Adapt to coq/coq#8933 (Make initial evar map argument to check_evars_are_solv...Gaë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