aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-29Merge PR #12929: Make abstract compatible with mangle namesPierre-Marie Pédrot
Reviewed-by: jashug Reviewed-by: ppedrot
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-28Merge PR #12933: Add test for past anomalyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-28Name saved goals in name_mangling testGaëtan Gilbert
Should be more robust with async proofs
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
Fix #12928 Fix #3146
2020-08-28About: Add a mention that arguments have been renamed, if ever it is the case.Hugo Herbelin
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
2020-08-28Where there are several lists of implicit arguments, don't pretend names matter.Hugo Herbelin
That is, in "About", use _ for the variables of the extra lists. See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
2020-08-28Do not write "rename" for arguments in About, since these arguments are ↵Hugo Herbelin
validated.
2020-08-28When printing the type in About, use the renamed arguments.Hugo Herbelin
2020-08-28When reporting an implicit argument error on a rename argument, use the ↵Hugo Herbelin
renaming. Example: > Arguments id [B] {b} : rename. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Argument B is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
2020-08-28Add test for past anomalyGaëtan Gilbert
Close #5703 I have no idea when this got fixed.
2020-08-28par: print relevant subgoal when failingGaëtan Gilbert
Fix (partial) #5502
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: proux01
2020-08-27Merge PR #12499: Clean future goalsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ↵coqbot-app[bot]
arguments of notations Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
We used to be refreshing the names for intros but not using the refreshed names. The same pattern of `intro_using` (which is what `intros ?name` effectively is) messing things up as in coq/coq#12881.
2020-08-26Add test for #10939Maxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Merge PR #12881: Deprecate intro_usingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
Reviewed-by: Zimmi48
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
Fix #12676
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
Fix #12889
2020-08-25[test-suite] close the proofEnrico Tassi
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its ↵Hugo Herbelin
documentation Reviewed-by: SkySkimmer Reviewed-by: herbelin Reviewed-by: jfehrle
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
Reviewed-by: mattam82 Ack-by: ppedrot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-08-24Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer ↵coqbot
exist Reviewed-by: SkySkimmer
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence ↵Pierre-Marie Pédrot
of artificial dependencies disappearing by reduction Reviewed-by: ppedrot
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to ↵Pierre-Marie Pédrot
be added Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
Reviewed-by: SkySkimmer Ack-by: gares
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
We fix it by reducing K-redexes the same in the both places (make_tuple and minimal_free_rels) which compute the dependencies of a dependent equality.
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-19Improve `make approve-output`Jason Gross
It now silently does nothing rather than erroring with `mv: cannot stat 'output/*.out.real': No such file or directory` if there is no output to approve, and also correctly handles `output-coqtop` and `output-coqchk` rather than ignoring these directories. Fixes #12863
2020-08-19[coqchk] Look inside inner modules as wellJason Gross
Fixes #12845 (coqchk reports names from inner modules of opaque modules as axioms) I don't fully understand the code here, so I can't speak as to its correctness, but it should be simple enough that reviewers can understand what it's doing and whether or not it's correct. This is useful for me in making progress towards https://github.com/mit-plv/fiat-crypto/issues/736
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
When calling an Ltac function, add specific locations when interpreting the function, when interpreting the arguments and when executating the call (in a TacArg).
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the ↵Martin Bodin
test files. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-08 15:03:16 +0000