aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Collapse)Author
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-02-17[coqdep] Tweak changelog after recent PRs.Emilio Jesus Gallego Arias
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-16Adding change log.Hugo Herbelin
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still ↵Emilio Jesus Gallego Arias
missing them. Reviewed-by: ejgallego
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-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-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-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-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-02-04Add changelog for non maximal implicit argsSimonBoulier
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-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-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-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Fix typo in changelog entry.Théo Zimmermann
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
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-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
Reviewed-by: maximedenes
2020-01-17Remove the CoqIDE "Revert all Buffers" command.Pierre-Marie Pédrot
Fixes #3907: CoqIDE File->Revert all buffers does not work. Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-01-17Remove the Tactic menu from CoqIDE.Pierre-Marie Pédrot
Partial fix of #11219: CoqIDE tactics and templates menus are out of sync. Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
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-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-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 Set NativeCompute TimingJason Gross
The command `Set NativeCompute Timing` causes calls to `native_compute` (as well as kernel calls to the native compiler) to emit separate timing information about compilation, execution, and reification. This allows more fine-grained timing of the native compiler without needing to set the `-debug` flag.
2020-01-08Add changelog entry for native string extractionMaxime Dénès
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-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
2020-01-07Trailing implicit error: changelogSimonBoulier
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 21:33:07 +0000