aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-21Merge PR #11425: Miscellaneous typosThéo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-01-21Reference manual: Typos/English in chapter universe polymorphism.Hugo Herbelin
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-19Merge PR #11398: Fix issue #11396 : Rlist hides standard list constructors ↵Pierre-Marie Pédrot
cons and nil Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
This partially fixes #10139 ; we now build the Ltac2 documentation and deploy it. The fix here can be used for inspiration to do the make-based part.
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
Reviewed-by: maximedenes
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-14Merge PR #11370: [zify] elim let in MLPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with ↵Hugo Herbelin
decorations Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
Fixes #10909: Set Default Proof Mode is not documented.
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to ↵Kazuhiko Sakaguchi
OCaml's string type Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: herbelin Ack-by: maximedenes Reviewed-by: pi8027
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
We make a temporary directory for these files and cleanup at process exit. The temporary directory means we don't have to guess what extensions ocaml will produce, we can just delete everything there. We use Lazy to avoid spamming unused directories when ahead-of-time compiling without actually using native casts / nativenorm (typically stdlib files). Sadly ocaml has "create temp file" but not "create temp dir", so we have to copy the name generation code. Fix #10495
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio ↵Pierre-Marie Pédrot
(and not just… Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: maximedenes
2020-01-10missing spaceOlivier Laurent
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
Close #11036
2020-01-08Add changelog entry for native string extractionMaxime Dénès
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Add documentation for extraction of ascii and string literalsMaxime Dénès
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
As suggested during review. That's a much better name.
2020-01-08Hide ExtrOcamlStringPlus.v like the other extraction filesXavier Leroy
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
2020-01-08Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rstSimonBoulier
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
2020-01-07Trailing implicit error: documentationSimonBoulier
2020-01-07Trailing implicit error: changelogSimonBoulier
2020-01-06doc: mention limitation of bidi hints vs programGaëtan Gilbert
No example as I'm not familiar enough with Program to make one.
2020-01-06[micromega] fix of bug #11191Frédéric Besson
- Add an instance to ZifyInst to instruct zify that 0 < x -> 0 < y -> 0 < Z.pow x y - More aggressive interval analysis to bound non-linear monomials.
2020-01-06Merge PR #11361: Fix #11360: discharge of template inductive with param only ↵Pierre-Marie Pédrot
use of var Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵Clément Pit-Claudel
migration. Reviewed-by: jfehrle
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
Reviewed-by: gares
2020-01-03coq_makefile: don't use CAMLPKGS when building cmxa of mllibGaëtan Gilbert
It seems broken according to unicoq experiences https://gitter.im/coq/coq?at=5e0e3e0005298604982ac3f7 Building cmxa of mlpack is already this way.
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
Closes #10491 We re-add the header in doc/tools/coqrst/notations/fontsupport.py which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6 The fontsupport script itself has been kept for reference, however it is not involved by any build target as of today.
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default ↵Pierre-Marie Pédrot
clauses in pattern matching decompilation algorithm Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29[refman] Fix bad quoting practice leftover from Sphinx migration.Théo Zimmermann
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the ↵Théo Zimmermann
Vernacular section to prodns Reviewed-by: Zimmi48
2019-12-29Merge PR #11183: Enhance prodn in .rst doc files to support multiple ↵Théo Zimmermann
productions in a prodn Ack-by: Zimmi48 Ack-by: cpitclaudel
2019-12-28Prevent apostrophes and backticks from being stylized in latexJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:30:47 +0000