aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-07Merge PR #8926: Move features that were not backported to 8.9 to the 8.10 sec...Guillaume Melquiond
2018-11-06Move features that were not backported to 8.9 to the 8.10 section of CHANGES.md.Théo Zimmermann
2018-11-06Merge PR #8889: Program hook gives back an obligation substitiutionPierre-Marie Pédrot
2018-11-06Merge PR #8912: [dune] [coqide] Use copy action instead of (run cp ...)Théo Zimmermann
2018-11-06Merge PR #8903: [dune] Add to vo rules explicit location of coqlib in boot mode.Théo Zimmermann
2018-11-06Merge PR #8884: Improve rendering of the credits.Théo Zimmermann
2018-11-06Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)Maxime Dénès
2018-11-06Merge PR #8915: More cleanup of vendored camlp5Emilio Jesus Gallego Arias
2018-11-06Removing dead code in Plexing.Pierre-Marie Pédrot
2018-11-06Remove the non-functorial interface of camlp5 grammars.Pierre-Marie Pédrot
2018-11-06Add overlay for EquationsMatthieu Sozeau
2018-11-06[program] extend obligation to give back a mapping from obligations toMatthieu Sozeau
2018-11-06Improve rendering of the credits.Guillaume Melquiond
2018-11-06Merge PR #8907: Cleanup camlp5 dead codeEmilio Jesus Gallego Arias
2018-11-06[dune] [coqide] Use copy action instead of (run cp ...)Emilio Jesus Gallego Arias
2018-11-05Remove patches of dead code in Gramlib.Pierre-Marie Pédrot
2018-11-05Remove the Scut constructor from Gramlib.Pierre-Marie Pédrot
2018-11-05Remove the Sflag constructor from Gramlib.Pierre-Marie Pédrot
2018-11-05Remove the Sfacto constructor from Gramlib.Pierre-Marie Pédrot
2018-11-05Remove the Svala constructor from Gramlib.Pierre-Marie Pédrot
2018-11-05Remove Smeta constructor in Gramlib.Pierre-Marie Pédrot
2018-11-05[dune] Add to vo rules explicit location of coqlib in boot mode.Emilio Jesus Gallego Arias
2018-11-05Merge PR #8899: Remove the deprecated Token module and port the corresponding...Emilio Jesus Gallego Arias
2018-11-05Merge PR #8815: NArith: add lemmas about numbers and vectorsHugo Herbelin
2018-11-05Merge PR #8871: [library] Move Nametab/Lib specific-names to NametabHugo Herbelin
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker.Gaëtan Gilbert
2018-11-05Merge PR #8896: Expose Typing.judge_of_applyPierre-Marie Pédrot
2018-11-05Merge PR #8866: Check universe instances in TypingPierre-Marie Pédrot
2018-11-05Merge PR #8824: Do not check convertibility of pattern types in the kernelMaxime Dénès
2018-11-05Merge PR #8874: Fix #8873: coqchk on inductive with letin parameterPierre-Marie Pédrot
2018-11-05Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in cas...Pierre-Marie Pédrot
2018-11-05Merge PR #8857: [library] Better sizing for libobject hashtbl.Pierre-Marie Pédrot
2018-11-05Merge PR #8766: [nametab] [api] Provide basic support for efficient completion.Pierre-Marie Pédrot
2018-11-05Merge PR #8836: [default.nix] Add coq-version and setupHook.Vincent Laporte
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-11-05Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel fu...Maxime Dénès
2018-11-05Merge PR #8843: Remove coqide ml4Pierre-Marie Pédrot
2018-11-05[default.nix] Update pinned nixpkgs.Théo Zimmermann
2018-11-05[default.nix] Add coq-version, meta.platform and setupHook.Théo Zimmermann
2018-11-04Remove the deprecated Token module and port the corresponding code.Pierre-Marie Pédrot
2018-11-03Merge PR #8877: Fix #8876: expected number of arguments for cumulative constr...Pierre-Marie Pédrot
2018-11-03Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to interpretatio...Pierre-Marie Pédrot
2018-11-03Merge PR #8844: Move abstract out of tactics.mlPierre-Marie Pédrot
2018-11-03Merge PR #8852: Use the obligation evar flagPierre-Marie Pédrot
2018-11-02Merge PR #8834: [error printing] Fix improper grounding of open terms in prin...Hugo Herbelin
2018-11-02Merge PR #8895: gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlPierre-Marie Pédrot
2018-11-02Merge PR #8809: [dev doc] Update proof engine docs, fixes #6640Pierre-Marie Pédrot
2018-11-02Expose Typing.judge_of_applyGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 04:28:51 +0000