aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-04-02Update coq_makefile timing testJason Gross
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-04-02Make OrderedTypeFullFacts a module functorSimon Gregersen
2018-04-02[lib] Move global options to their proper place.Emilio Jesus Gallego Arias
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-04-02[coq] Adapt to coq/coq#6960.Emilio Jesus Gallego Arias
2018-04-01Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHEN...Pierre-Marie Pédrot
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-04-01Merge PR #7132: [doc] Add some more documentation to STM API.Enrico Tassi
2018-04-01Merge PR #6802: Remove deprecated commands Implicit Arguments and Arguments S...Enrico Tassi
2018-04-01[toplevel] Protect goal printing better wrt Break [fixes #7142]Emilio Jesus Gallego Arias
2018-04-01[stm] More cleanup of "classification is not an interpreter"Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-31[doc] Add some more documentation to STM API.Emilio Jesus Gallego Arias
2018-03-31Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh)Emilio Jesus Gallego Arias
2018-03-30Add CHANGES for removing Implicit Arguments and Arguments ScopeJasper Hugunin
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-31Merge PR #7121: Remove outdated patch from ci-sfEmilio Jesus Gallego Arias
2018-03-31Merge PR #6989: Enable whitespace checking for new Sphinx file extensions.Emilio Jesus Gallego Arias
2018-03-31Merge PR #7111: Fix #6631: Derive Plugin gives "Anomaly: more than one statem...Emilio Jesus Gallego Arias
2018-03-31Linter: verify overlay extensions.Gaëtan Gilbert
2018-03-31pre-commit: verify user overlay extensions (must be .sh).Gaëtan Gilbert
2018-03-31Merge PR #7130: gitlab: fix environment for build templateEmilio Jesus Gallego Arias
2018-03-30[Sphinx] Add chapter 27Maxime Dénès
2018-03-30[Sphinx] Move chapter 27 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Add chapter 25Maxime Dénès
2018-03-30[Sphinx] Move chapter 25 to new infrastructureMaxime Dénès
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
2018-03-30gitlab: fix environment for build templateGaëtan Gilbert
2018-03-30Adding some headers, by consistency of style.Hugo Herbelin
2018-03-29Remove outdated patch from ci-sfJasper Hugunin
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
2018-03-29[Sphinx] Add chapter 26Maxime Dénès
2018-03-29[Sphinx] Move chapter 26 to new infrastructureMaxime Dénès
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
2018-03-29Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Pierre-Marie Pédrot
2018-03-29[Sphinx] Add chapter 24Maxime Dénès
2018-03-29[Sphinx] Move chapter 24 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Add chapter 23Maxime Dénès
2018-03-29[Sphinx] Move chapter 23 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Remove duplicate entry for command `Coercion`Maxime Dénès
2018-03-29[Sphinx] Add chapter 18Maxime Dénès
2018-03-29[Sphinx] Move chapter 18 to new infrastructureMaxime Dénès
2018-03-29Merge PR #7057: Sphinx Chapter 20: Type ClassesMaxime Dénès
2018-03-29Merge PR #7072: Update codeownersMaxime Dénès
2018-03-29Remove dev/doc/changes.md from files with a code owner.Théo Zimmermann
2018-03-29Preparing old-style refine from logic.ml to deal with "Cases" proofHugo Herbelin
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 02:54:59 +0000