aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-19Gramlib: Fixes #9358 (ensuring that the loc function has something to compute).Hugo Herbelin
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
2019-02-19Fix #9595: missing non-primitive-record warning with 0 field recordGaëtan Gilbert
2019-02-19Make inductive cumulativity flag local to vernacentriesGaëtan Gilbert
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18[sphinx] Add abort and restart options to directive coqtop.Théo Zimmermann
2019-02-18coqdomain.py fix typo in commentGaëtan Gilbert
2019-02-18Sphinx: nicer error reportingGaëtan Gilbert
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Sphinx: remove [coqtop:: undo]Gaëtan Gilbert
2019-02-18Fix last nested lemma failure.Théo Zimmermann
2019-02-18Fix failing coqtops in type-classes.rstGaëtan Gilbert
2019-02-18Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linterThéo Zimmermann
2019-02-18Merge PR #9589: Deprecate duplicated explicitation_eqEmilio Jesus Gallego Arias
2019-02-18Merge PR #9600: CI: fix trunk jobs switch pickingEmilio Jesus Gallego Arias
2019-02-18Merge PR #9597: [ci] Resolve commit corresponding to branch when downloading ...Emilio Jesus Gallego Arias
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-18Merge PR #9592: Fix per-commit linting with bot mergesEmilio Jesus Gallego Arias
2019-02-18Merge PR #9599: Remove undefined install_printer ppcumulativity_infoEmilio Jesus Gallego Arias
2019-02-18[dev] Add include versions for Dune builds.Emilio Jesus Gallego Arias
2019-02-18CI: fix trunk jobs switch pickingGaëtan Gilbert
2019-02-18Remove undefined install_printer ppcumulativity_infoGaëtan Gilbert
2019-02-18[ci] Resolve commit corresponding to branch when downloading tarball.Théo Zimmermann
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaëtan Gilbert
2019-02-18Merge PR #9590: [gitlab] [docker] [ci] Remove "edge" compiler switch.Gaëtan Gilbert
2019-02-18Fix per-commit linting with bot mergesGaëtan Gilbert
2019-02-18Merge PR #9439: Separate variance and universe fields in inductives.Pierre-Marie Pédrot
2019-02-18Merge PR #9509: Fix #9508: Unexpected interaction between implicit arguments ...Maxime Dénès
2019-02-18[Namegen] Use Global.exists_objlabel in `next_global_ident_away`Vincent Laporte
2019-02-18[gitlab] [docker] [ci] Remove "edge" compiler switch.Emilio Jesus Gallego Arias
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
2019-02-17Merge PR #9549: [ide] fix unconditional goto-point on editing an error (fix #...Pierre-Marie Pédrot
2019-02-17Merge PR #9506: Remove some non tailrec List.map from CList implementationsPierre-Marie Pédrot
2019-02-16Deprecated duplicated explicitation_eqJasper Hugunin
2019-02-16Add links for all mentions of Gitter and Discourse.Théo Zimmermann
2019-02-16Fix English grammar.Jason Gross
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-14Adapt to coq/coq#8817 (SProp)Gaëtan Gilbert
2019-02-14Document the now_show tactic.Théo Zimmermann
2019-02-14Merge PR #9502: Remove nondeterministic testsThéo Zimmermann
2019-02-14Merge PR #9542: [Manual] Don’t use `Undo`; and other cleaningThéo Zimmermann
2019-02-14[Manual] Fix a referenceVincent Laporte
2019-02-14[Manual] Clean examples for `apply`Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 06:07:13 +0000