diff options
| author | coqbot-app[bot] | 2020-11-12 14:46:58 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-12 14:46:58 +0000 |
| commit | 6d7877829b7265d6c416c17ea3bbacf65f306609 (patch) | |
| tree | 106990d1eb961d61b09f137be6759d663aa13b39 /test-suite | |
| parent | 7ba09858a87a6940278c96ae328e44c142842cd9 (diff) | |
| parent | b9f4ed819b36cfa27046743035fa080035db6672 (diff) | |
Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, not only on subidentifiers of an identifier
Reviewed-by: Zimmi48
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Search.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 6 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index ef4c6bac93..0f5fd91d93 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -462,3 +462,7 @@ inr: forall {A B : Type}, B -> A + B inl: forall {A B : Type}, A -> A + B (use "About" for full details on the implicit arguments of inl and inr) f: None = 0 +partition_cons1: + forall [A : Type] (f : A -> bool) (a : A) (l : list A) [l1 l2 : list A], + partition f l = (l1, l2) -> + f a = true -> partition f (a :: l) = (a :: l1, l2) diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2f29e1aff1..3419d5ac62 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -96,3 +96,9 @@ Module WithCoercions. Axiom f : None = 0. Search (None = 0). End WithCoercions. + +Require Import List. + +Module Wish13349. +Search partition "1" inside List. +End Wish13349. |