aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Collapse)Author
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
Fixes #12582 The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime `plik.v.log` is older than `Nat.vo`. This is circular, and results in `make` considering all of the `modules/` tests out-of-date on any fresh run.
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
Fixes #12571.
2020-06-23Merge PR #12562: CoqIDE: accept to open files with invalid namesMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: SkySkimmer
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Fix 12483Pierre Roux
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not ↵Emilio Jesus Gallego Arias
deprecation. Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: jfehrle
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-29Change log for #12422.Hugo Herbelin
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-27Adding changelog.Martin Bodin
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-27Fix changelog for #11986.Théo Zimmermann
2020-05-26Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugsGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
Fixes #12386
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-22[coqchk] Fix #5030Pierre Roux
When encountering ```Coq Module M : T. ... Lemma c :... ... Qed. ... End M. ``` every field `c` without body in `T` but with a body in `M` is registered as opacified in a table along with all constants `opacified(c)` without body in the environment at this point (i.e., all axioms potentially used by c). Then, when printing axioms, if `c` appears in the final environment it is replaced by `opacified(c)` in the resulting list of axioms.
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with ↵Pierre-Marie Pédrot
eta-expansion of "match" branches Reviewed-by: gares Ack-by: ppedrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-21Fix an uncaught python exception in timingJason Gross
Previously, when either the 'before' or 'after' had no files, we'd get an uncaught exception: ``` Traceback (most recent call last): File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in <module> table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem) File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) ValueError: max() arg is an empty sequence ``` Fixes #12387
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-20Print a newline at the end of timing tablesJason Gross
This, for example, improves the CI display, so that `$ echo 'end:coq.test'` does not appear on the same line as the end of the timing table.
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
Closes #12351. We set the parameters of the redirect formatter to be same than the ones in stdout. I guess the original semantics was to ignore the parameters, so I'm unsure we want to do this. While we are a it, we include a fix on the formatter, which _must_ be flushed before closing its associated channel.
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
Fixes #11936. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ↵Jason Gross
reductions Reviewed-by: JasonGross Ack-by: Zimmi48
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
Error happened only when writing: functional induction f x y z. instead of functional induction (f x y z). Now the former is equivalent to the former: implicits must be omitted. Hence small source of incompatibility, but a more homogeneous behaviour.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:44:59 +0000