aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-20[doc] Skip unneeded copies in copy_formatspecific_filesClément Pit-Claudel
2018-09-20[doc] Move a citation back into the introductionClément Pit-Claudel
Alternatively, we could duplicate the citation text in both index files.
2018-09-20[doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targetsClément Pit-Claudel
2018-09-20[doc] Remove frames around code snippets in the LateX buildClément Pit-Claudel
2018-09-20[doc] Change the name that appears on the first page of the PDF manualClément Pit-Claudel
2018-09-20[doc] Fix some Sphinx LaTeX warnings and silence othersClément Pit-Claudel
2018-09-20[doc] Add another common mistake to the documentation-writing guideClément Pit-Claudel
2018-09-20[doc] Fix a few syntax highlighting issuesClément Pit-Claudel
2018-09-20[doc] Get rid of two Sphinx warningsClément Pit-Claudel
2018-09-20[doc] Fix more duplicate-label issues in production listsClément Pit-Claudel
2018-09-20[doc] Rewrite and document the prodn directiveClément Pit-Claudel
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
2018-09-20[doc] Add more common mistakes to the documentation-writing guideClément Pit-Claudel
2018-09-20[doc] Mark the dummy index files as orphans (the LaTeX build skips them)Clément Pit-Claudel
Do we really need these? Wouldn't it be better to just add appropriate links to the html template?
2018-09-20[doc] Add a warning about overusing the `coqtop` directiveClément Pit-Claudel
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979Clément Pit-Claudel
2018-09-20[doc] Ensure that merging coqtop blocks preserves anchorsClément Pit-Claudel
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980Clément Pit-Claudel
2018-09-20[doc] Fix a typo in the developer guideClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Improve rendering of Coq objects in PDF outputClément Pit-Claudel
2018-09-20[doc] Add env_version to metadata of coqrst pluginClément Pit-Claudel
This is required by Sphinx 8.0. See https://github.com/sphinx-doc/sphinx/issues/4460.
2018-09-20[doc] Fix a few LaTeX mistakesClément Pit-Claudel
2018-09-20[doc] Create a wrapper around the Credits file for the LaTeX buildClément Pit-Claudel
2018-09-20[doc] Create a separate zebibliography file for the LaTeX buildClément Pit-Claudel
`.. bibliography::` puts the bibliography on its own page with its own title in LaTeX, but includes it inline without a title in HTML [1], so we need to maintain two separate copies of zebibliography.rst [1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
2018-09-20[doc] Create a separate index file for the LaTeX buildClément Pit-Claudel
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
2018-09-20[doc] Remove an empty '.. bibliography::' in addendum/programClément Pit-Claudel
2018-09-20[doc] Explain why zebibliography needs to be separate and oddly-namedClément Pit-Claudel
2018-09-20[doc] Adjust conf.py to allow LaTeX buildsClément Pit-Claudel
2018-09-20[doc] Move the LaTeX preamble to a separate .tex fileClément Pit-Claudel
2018-09-20[doc] Fix a typo in coqdomain.pyClément Pit-Claudel
2018-09-19Move tests in bugs/ to the bugs/closed/.Nick Lewycky
2018-09-19Fix Numeral Notations (4/4 - fixing synch)Jason Gross
This fixes #8401 Supersedes / closes #8407 Vernacular-command-registered numeral notations now live in the summary, and the interpretation function for them is hard-coded. Plugin-registered numeral notations are still unsynchronized, and only the UIDs of these functions gets synchronized. I am not 100% sure why this is fine, but the test-suite file working suggests that it is fine. I think it is because worker delegation correctly handles non-synchronized state which is declared at `Declare ML Module`-time. This final commit changes the synchronization of numeral notations (and deletes no-longer-used declarations in notation.mli that were introduced temporarily in the last commit). Since the interpretation can now be done in notation.ml, we no longer need to register unique ids for numeral notation (un)interp functions, and can instead synchronize the underlying constants with the document state. This is the change that actually fixes #8401.
2018-09-19Fix Numeral Notations (3/4 - moving more stuff)Jason Gross
Move most of the rest of the stuff from numeral.ml to notation.ml. Now that we use exceptions to print error messages, all of the interpretation code for numeral notations can be moved to notation.ml. This is commit 1/4 in the fix for #8401. This is a pure cut/paste commit, modulo fixing name qualifications due to moved things, and exposing some stuff in notation.mli (to be removed in the next commit, where we finish the numeral notation reworking).
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
Switch to using exceptions rather than user errors. This will be required because the machinery for printing constrs is not available in notation.ml, so we move the error message printing to himsg.ml instead. This is commit 2/4 in the fix for #8401.
2018-09-19Fix Numeral Notations (1/4 - moving things)Jason Gross
Move various things from from numeral.ml to notation.ml and notation.mli; this is required to allow the vernac command to continue living in numeral.ml while preparing to move all of the numeral notation interpretation logic to notation.ml This is commit 1/4 in the fix for #8401. This is a pure cut/paste commit, modulo adding section-heading comments.
2018-09-19Merge PR #8505: Fix Windows builds: OPAM has changed its URL schema.Michael Soegtrop
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic ↵Enrico Tassi
independent of the multi-usage internal "letin_tac"
2018-09-19[ssr] use the right environment in ssrpattern (fix #8454)Enrico Tassi
2018-09-19Fix Windows builds: OPAM has changed its URL schema.Théo Zimmermann
2018-09-19Merge PR #7343: Add missing index entries.Maxime Dénès
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-19Replace trivial uses of declare_summary with summary.refsGaëtan Gilbert
The one in notation.ml looks trivial but is needed to do with_notation_protection (used by inductive/fixpoint local notations).
2018-09-19Remove Hints.add_hints_initGaëtan Gilbert
It was only used in ltac/rewrite which as a plugin is too late to affect init.
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-19Merge PR #8071: Propose a Code of Conduct for Coq.Matthieu Sozeau
2018-09-19Merge PR #7257: Fixing yet a source of dependency on alphabetic order in ↵Pierre-Marie Pédrot
unification.
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-19Merge PR #8463: Remove DischargedhypsmapsPierre-Marie Pédrot
2018-09-18[api] Deprecate two forgotten print functions that use global state.Emilio Jesus Gallego Arias
Removal of the global state API is scheduled for 8.10, thus it is crucial we ship this in 8.9.
2018-09-18Merge PR #8486: Mising prime in the subtyping rulesThéo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:53:44 +0000