aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-17Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` viewCyril Cohen
Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
Fixes #12529
2020-06-16make the linter happyEnrico Tassi
2020-06-15[ssr] fix env handling in error message (fix #12507)Enrico Tassi
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-11[test-suite] [stm] Interactive test case for fail-on-qed.Emilio Jesus Gallego Arias
2020-06-11Merge PR #12443: Fix #12442: Confusing error message when the intro pattern ↵Pierre-Marie Pédrot
of "apply in" fails Reviewed-by: ppedrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n ↵Vincent Semeria
to 1/2^n Reviewed-by: VincentSe
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Fix 12483Pierre Roux
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
Fix #12447
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
Fixes #12390
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-06-01Slight improvement in naming existential variables.Hugo Herbelin
In a Meta := Evar unification problem and the Meta is bound to a (named) binder, and the Evar is a GoalEvar, we set the source of the evar to be the one of the Meta.
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
This is a quick fix to avoid the anomaly, with a fallback on before b1b8243b7fc.
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async ↵Emilio Jesus Gallego Arias
mode. Reviewed-by: JasonGross Reviewed-by: ejgallego
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
In this mode, an additional error was emitted, which made the test fail: Error: There are pending proofs: Unnamed_thm.
2020-05-22[coqchk] Add testPierre Roux
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-21Merge PR #12358: [topfmt] Set formatter + flush fixGaëtan Gilbert
Reviewed-by: JasonGross Reviewed-by: SkySkimmer Ack-by: Zimmi48
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-20Merge PR #12350: [test-suite] Ensure copies of files are writableGaëtan Gilbert
Reviewed-by: SkySkimmer
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-18Merge PR #12289: test-suite: fix bug causing unit tests to be skippedHugo Herbelin
Reviewed-by: herbelin
2020-05-18[test-suite] Ensure copies of files are writableEmilio Jesus Gallego Arias
This is needed for the case the sources are set to read-only mode, for example when using Dune >= 2.5 [needed for the global cache support] Fixes #12264 Co-authored-by: Ignat Insarov <kindaro@gmail.com>
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-18Merge PR #11980: Improve spacing in Print AssumptionsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: herbelin
2020-05-18Merge PR #12345: test-suite/Makefile: fix incomplete prerequisite listEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-18test-suite/Makefile: fix incomplete prerequisite listGaëtan Gilbert
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
cf "If this is implemented, long names might cause a printing problem:" in #11852
2020-05-17Revert "[test] unit tests for ide/coq_lex.ml" + makefile supportGaëtan Gilbert
This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and 0976a670cf853c9bc61b3eee6dceae4a429e066f.
2020-05-17Fix proof_diffs_test.mlGaëtan Gilbert
2020-05-17test-suite: fix bug causing unit tests to be skippedGaëtan Gilbert
Since `ocaml_pwd.ml` was added this unquoted glob would be expanded by the shell before being passed to `find`.
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
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.
2020-05-15Test new Search features.Théo Zimmermann
2020-05-15Deprecate SearchHead.Théo Zimmermann
The main use case of SearchHead is now handled by headconcl: The secondary use case was redundant with SearchPattern.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:42:31 +0000