aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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
2019-02-14[Manual] Don’t use `Undo` in ssreflect examplesVincent Laporte
2019-02-14[Manual] Clean examples about `inversion` tacticVincent Laporte
2019-02-13Merge PR #9554: Don't save expected failure logs from opened/ bugs.Maxime Dénès
2019-02-13Merge PR #9450: Fix #9432: canonical structure and coercion accept universe b...Maxime Dénès
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-13more testsEnrico Tassi
2019-02-13refactor grammarEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
2019-02-13Merge PR #9557: [ssreflect] Export more parsing witnesses.Enrico Tassi
2019-02-13Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.Maxime Dénès
2019-02-12Merge PR #9548: Almost fully type-safe gramlib implementationEmilio Jesus Gallego Arias
2019-02-12Merge PR #9563: Improve the documentation of auto.Clément Pit-Claudel
2019-02-12Fix failing coqtops in syntax-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coqide.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coq-library.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Improve the documentation of auto.Théo Zimmermann
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-12Fix undefined SPHINX_DEPS when QUICKGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:19:56 +0000