aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo Herbelin
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
- merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
The previous implementation appears to be sound when Mangle Names is off, but it relies on two fragile assumptions, namely that next_global_ident_away always returns different identifiers when called with naming hints which are different after stripping all digits from the end, and that default_id_of_sort (locally defined) never returns "HC" or "P", or either of those followed by a string of digits. These changes make both assumptions unnecessary. As a side note, it seems odd that fresh is ignoring it's env parameter.
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable ↵Pierre-Marie Pédrot
from initial evars Ack-by: JasonGross Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵coqbot-app[bot]
in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see ↵Pierre-Marie Pédrot
comment in #12944). Ack-by: RalfJung Ack-by: jashug Reviewed-by: ppedrot
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
The test is refined to handle aliases: i.e. undefined evars coming from restrictions and evar-evar unifications with an initial evar are not considered fresh unresolved evars. To check this, we generalize the restricted_evars set to an aliased_evars set in the evar map, registering evars being solved by another evar due to restriction or evar-evar unifications. This implements the proposal of PR #370 for testing the resolution status of evars independently of the evar-evar orientation order. This allows [apply] to refine an evar with a new one if it results from a [clear] request or an evar-evar solution only, otherwise the new evar is considered fresh and an error is raised. Also fixes bugs #4095 and #4413. Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
2020-09-04Merge PR #12893: Fix incorrect debruijn handling when Record calls ↵coqbot-app[bot]
maybe_unify_params_in Reviewed-by: maximedenes
2020-09-04Merge PR #12912: Fix algebraic comparison with sprop on one sidePierre-Marie Pédrot
Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-09-03Fix incorrect debruijn handling when Record calls maybe_unify_params_inGaëtan Gilbert
Fix #12887
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-31Fix mangle names issue in inductionGaëtan Gilbert
Fix #12944
2020-08-31Fixes a freshness issue with induction (see comment in #12944).Hugo Herbelin
The names computed in consume_pattern were lost when calling intros_pattern_core. Moreover, the computation of names to avoid was done several time. We compute it once for all.
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-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
Fix #12930
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-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
Close #12909
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 17:24:17 +0000