aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-18Merge PR #8486: Mising prime in the subtyping rulesThéo Zimmermann
2018-09-18Merge PR #8485: Missing space in cic.rstThéo Zimmermann
2018-09-18Removing Dischargedhypsmap which is unused internally.Maxime Dénès
The Dischargedhypsmap table collected the segment of section variables that constants defined in a section were originally depending on. It was useful to reconstruct the structure of sections as originally given in a source file. In particular this was used in Sacerdoti Coen's plugin for exportation of Coq files to xml. There is no information that this plugin, moved out of Coq in September 2014, was finally maintained, even as an external plugin. So it seems that the Dischargedhypsmap table is virtually not used anymore in the wild. Please contact the developers if ever the need for such a table happens to be necessary for your work.
2018-09-17Add missing index entries.Théo Zimmermann
In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
2018-09-17Merge PR #6906: [VM] Optimize structured valuesPierre-Marie Pédrot
2018-09-17Merge PR #8053: [dune] Add apidoc target using `odoc`Gaëtan Gilbert
2018-09-17OCaml now exports the min and max non-constant tags, let's use itMaxime Dénès
2018-09-17Add assertion on tags in eq_structured_constantsMaxime Dénès
2018-09-17[VM] Allocate a bit less in digits_from_uintMaxime Dénès
2018-09-17[VM] Inject structured constants in values without reallocating them.Maxime Dénès
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
2018-09-16Mising prime in the subtyping rulesJoachim Breitner
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-15Overlay for cross-crypto.Hugo Herbelin
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
This refines even further c24bcae8 (PR #924) and 6304c843: - c24bcae8 fixed the order in the heuristic - 6304c843 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-14Merge PR #8326: Mention PRINT_LOGS=1 when failing test suiteEnrico Tassi
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-13Merge PR #8434: Canonical representation of kernel substitutionsMaxime Dénès
2018-09-13Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernelMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:36:00 +0000