aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic ↵Emilio Jesus Gallego Arias
definitions Reviewed-by: ejgallego Reviewed-by: herbelin
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
Apparently the `Timeout` exception is raised by a signal handled, and that can happen when the running thread is a worker manager, rather than the main thread (the one that should be interrupted). Given that the point of these tests is to test *auto and not the STM, we disable async proofs forcibly.
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
This should make the univbinders output test less fragile as it depends less on the global counter (still used for universes from section variables).
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-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
Reviewed-by: mattam82
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
Fixes #12571.
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
Reviewed-by: gares Reviewed-by: maximedenes
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
Reviewed-by: fajb
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential ↵Gaëtan Gilbert
variables in goals Reviewed-by: SkySkimmer
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 07:27:48 +0000