aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-02-13Merge PR #11098: Let Arguments support anonymous implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
This was already possible manually using "{ _ }" in the type of declaration. This was also possible for type classes. So, no reason to forbid in Arguments.
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
2020-02-11Update doc/sphinx/practical-tools/utilities.rstJason Gross
2020-02-11Document the ability to use manual implicit arguments in subexpressions.Hugo Herbelin
2020-02-11Lately adding a changelog for PR#10202.Hugo Herbelin
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
2020-02-08Remove -compat 8.9.Théo Zimmermann
Commit auto-generated by running dev/tools/update-compat.py --release. As per release doc this must be run at some point before branching (not necessarily close to the branching date).
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
Reviewed-by: herbelin Ack-by: jfehrle
2020-02-08Merge PR #10343: Resolve 10342 : [Ltac2] Add array libraryPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: ppedrot
2020-02-08Merge PR #11404: replace RList by list R in all files where it is used in ↵Pierre-Marie Pédrot
this directory Ack-by: SkySkimmer Reviewed-by: herbelin
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-07[coqdep] Add changelog for recent modifications.Emilio Jesus Gallego Arias
2020-02-06Apply suggestions from code reviewJason Gross
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-02-06replace RList by list RYves Bertot
add an overlay for coquelicot remove functions from RList: In, Rlength, cons_Rlist, app_RList because they are essentially the same as In, length, app, and map from List (beware that the order of arguments changes for map, and the In function contains reversed equalities). adds deprecation warnings for Rlist and Rlength adds deprecated notations for RList.cons and RList.nil
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
- Add a `--fuzz` option to `make-both-single-timing-files.py` Passing `--fuzz=N` allows differences in character locations of up to `N` characters when matching lines in per-line timing diffs. The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`. See also the discussion at https://github.com/coq/coq/pull/11076#pullrequestreview-324791139 - Allow passing `--real` to per-file timing scripts and `--user` to per-line timing script. This allows easily comparing real times instead of user ones (or vice versa). - Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build - We also now use argparse rather than a hand-rolled argument parser; there were getting to be too many combinations of options. - Fix the ordering of columns in Coq's build system; this is the equivalent of #8167 for Coq's build system. Fixes #11301 Supersedes / closes #11022 Supersedes / closes #11230
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-04Apply suggestions from HugoSimonBoulier
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-02-04Add changelog for non maximal implicit argsSimonBoulier
2020-02-04Update doc for non max implicit argumentsSimonBoulier
2020-02-03Fix efficiency regression #11436Frédéric Besson
- The cutting plane has been (sometimes) improved to generate stronger cuts. - There is now some support for profiling the Simplex see documentation for Show Lia Profile.
2020-02-02Merge PR #11466: checkdeps.py: add missing dep & report deps all at onceThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-30Merge PR #11464: Fix off-by-one in docs of `first num last` (fix #11463)Enrico Tassi
Reviewed-by: gares
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
This seems seldom used and I think in general instrumentation this way is pretty limited (usually better to use the build system to tweak) It thus seems worth removing as to simplify `Mltop` a bit, but of course comments are welcome.
2020-01-27Rephrase to reduce ambiguityPaolo G. Giarrusso
This is the smallest possible change to clarify the text without making it even more formal.
2020-01-27Fix off-by-one in docs of `first num last` (fix #11463)Paolo G. Giarrusso
2020-01-27checkdeps.py: report *all* missing dependencies at oncePaolo G. Giarrusso
Otherwise you need a few feedback loops to install all dependencies.
2020-01-27checkdeps: check for sphinxcontrib-bibtexPaolo G. Giarrusso
I lacked this package, and got: ``` $ make -j2 COQ_USE_DUNE=1 refman-html [...] env doc/sphinx_build (exit 2) (cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html) Running Sphinx v2.1.2 Extension error: Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex') make: *** [refman-html] Error 1 ```
2020-01-27Merge PR #11415: Remove the CoqIDE "Revert all Buffers" command.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: maximedenes
2020-01-23More minor tweaks to the 8.11 changelog.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-23Add missing 'and'.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-22Minor tweaks to the 8.11 changelog.Théo Zimmermann
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Fix typo in changelog entry.Théo Zimmermann
2020-01-22Insert changelog entry for #11430 from v8.11 branch.Théo Zimmermann
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
2020-01-22A few edits to the 8.11 section of the Changes chapter.Théo Zimmermann
- Mention Guillaume Claret among maintainers of the OPAM repository (as suggested by Karl Palmskog). - Update links to the documentation to avoid being outdated. - Mention sections beyond the one on 8.11+beta1.
2020-01-22Changelog for 8.11.0.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 17:55:00 +0000