aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-16Merge PR #7215: Deprecate the "simple subst" tactic.Hugo Herbelin
2018-04-16Merge PR #7263: CHANGES: document COQFLAGS changeEnrico Tassi
2018-04-16CHANGES: document COQFLAGS changeRalf Jung
2018-04-16Merge PR #7200: [ltac] Deprecate nameless fix/cofix.Maxime Dénès
2018-04-16Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacingMaxime Dénès
2018-04-16Merge PR #7246: Add missing CHANGES entry for #6169.Maxime Dénès
2018-04-15Merge PR #7247: Simplify CircleCI scriptGaëtan Gilbert
2018-04-15Merge PR #7252: Sphinx doc fix warningsThéo Zimmermann
2018-04-15Simplify CircleCI scriptYishuai Li
2018-04-14Merge PR #7250: Sphinx doc chapter 9Théo Zimmermann
2018-04-14[Sphinx] Build with warnings as errorsMaxime Dénès
Most of these warnings should really be errors (ill-formed input, invalid cross references, etc.) so we make it the default.
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14doc: Rename UbuntuMono-Square to CoqNotations and tweak spacingClément Pit-Claudel
The Ubuntu Font License requires substantially modified fonts to be renamed entirely.
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
2018-04-14[Sphinx] Add chapter 9.Théo Zimmermann
Chapter ported by Théo Zimmermann and Maxime Dénès.
2018-04-14[Sphinx] Move chapter 9 to new infrastructure.Théo Zimmermann
2018-04-14Merge PR #7136: Evar maps contain econstrs.Pierre-Marie Pédrot
2018-04-14Merge PR #7217: Sphinx doc chapter 1Théo Zimmermann
2018-04-14Add missing CHANGES entry for #6169.Théo Zimmermann
Fixes #7243.
2018-04-13Overlay for econstr in Evd.Gaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵Pierre-Marie Pédrot
contains evars
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
2018-04-13[Sphinx] Add Chapter 1Maxime Dénès
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
2018-04-13Merge PR #7117: Sphinx doc chapter 29Théo Zimmermann
2018-04-13Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods.Enrico Tassi
2018-04-12Merge PR #7222: [sphinx] Remove migration artefacts.Maxime Dénès
2018-04-12Merge PR #7194: [warnings] Remove `set_current_loc` hack.Maxime Dénès
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵Jason Gross
removing the test.
2018-04-12Merge PR #7202: Correction of ugly message described in #4667Pierre Courtieu
2018-04-12Merge PR #7220: Many Sphinx fixes (including a fix of the credits chapter)Maxime Dénès
2018-04-12Merge PR #7201: Translation fixes in chapter syntax extensions.Maxime Dénès
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-12Merge PR #500: Move bugs that have been closed on BugzillaMaxime Dénès
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
The "Stream.Error" printer does add a period, so, the messages themselves should not.
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-12Merge PR #7096: coqide: avoid marking sentences that are not in the document ↵Pierre-Marie Pédrot
anymore
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac ↵Pierre-Marie Pédrot
failure in other file
2018-04-12[Sphinx] Add chapter 29Maxime Dénès
Thanks to Clément Pit Claudel for porting this chapter. Backport universe polymorphism changes from 2017 and 2018.
2018-04-11[sphinx] Remove migration artefacts.Théo Zimmermann
These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target.
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-11[sphinx] Use macros for notes and examples.Théo Zimmermann
2018-04-11[sphinx] Fixes in chapter 2.Théo Zimmermann
Mostly using the good option macros.
2018-04-11Remove empty reference to the current version of Coq.Théo Zimmermann
2018-04-11[sphinx] Use macro |CoqIDE| consistently.Théo Zimmermann
2018-04-11Add credits related to the Sphinx migration.Théo Zimmermann
Closes #7209.
2018-04-11Correction of ugly message described in #4667Julien Forest
2018-04-11Fix wrong mention in the release notes.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:04:51 +0000