aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-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.
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Search: Displaying the "use About" notice only when really needed.Hugo Herbelin
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with ↵Emilio Jesus Gallego Arias
implicit types Reviewed-by: ejgallego
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ↵Hugo Herbelin
runtime. Reviewed-by: herbelin
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
See #11840 for a motivation. I had to fix Floats.FloatLemmas because it uses the same name for a notation and a term, and the fact this unfold was working on this was clearly a bug. I hope nobody relies on this kind of stuff in the wild. Fixes #5764: "Cannot coerce ..." should be a runtime error. Fixes #5159: "Cannot coerce ..." should not be an error. Fixes #4925: unfold gives error on Admitted.
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
We take the env of the current goal with the context replaced with section variables. In practice, this is the global env, but, maybe, one day, a goal state will have its own env.
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
A pattern-matching clause was missing in 5f314036e4d (PR #11261). The anomaly triggered in configurations like "fun (x:T) y => ..." (even in the absence of "Implicit Types").
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: mattam82
2020-05-14Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 06:28:19 +0000