aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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-02Remove ml4 from Coq's make build systemGaëtan Gilbert
2018-11-02Select OS specific coqide code with cp.Gaëtan Gilbert
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
2018-11-02[dev doc] Update proof engine docs, fixes #6640Emilio Jesus Gallego Arias
2018-11-01Merge PR #8845: Fix typos in the document about CICThéo Zimmermann
2018-10-31Fixes rest of #3468 (tactic-in-term was not respecting scopes).Hugo Herbelin
2018-10-31Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).Hugo Herbelin
2018-10-31Use standard combinator for Global.set_strategyMaxime Dénès
2018-10-31Introduce Safe_typing.set_share_reductionMaxime Dénès
2018-10-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-10-31Merge PR #8752: Enable fragile pattern warning in cclosureMaxime Dénès
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
2018-10-31Merge PR #8841: Share the construction of the evar instance in Clenv.make_eva...Matthieu Sozeau
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
2018-10-31Merge PR #8867: Notations: fixing a bug when printing abbreviations in custom...Emilio Jesus Gallego Arias
2018-10-31Merge PR #8864: Avoid passing empty environmentsPierre-Marie Pédrot
2018-10-31Merge PR #8688: Generalizing the various evar_map printers in Termops over an...Pierre-Marie Pédrot
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
2018-10-31[library] Better sizing for libobject hashtbl.Emilio Jesus Gallego Arias
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-10-31Merge PR #8851: Credits for 8.9Guillaume Melquiond
2018-10-31Merge PR #8849: Fix for bug #8848.Pierre-Marie Pédrot
2018-10-30Merge PR #8750: [ci] [doc] Notes about branch names.Gaëtan Gilbert
2018-10-30Credits for 8.9Matthieu Sozeau
2018-10-30Overlays (#8844 split-tactics)Gaëtan Gilbert
2018-10-30Adding overlay for coq-elpiHugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
2018-10-30Remove fully_empty_glob_sign which uses a dummy environmentMaxime Dénès
2018-10-30Avoid passing dummy env to error printerMaxime Dénès
2018-10-30Reduction functions based on CClosure should take an envMaxime Dénès
2018-10-30Remove one use of empty_env in ssrMaxime Dénès
2018-10-30Avoid redefining reduction functions in fun_indMaxime Dénès
2018-10-30Distinguish globalization and pretyping error on unbound variableMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:09:57 +0000