diff options
| author | Cyril Cohen | 2020-11-18 02:01:45 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-18 02:01:45 +0100 |
| commit | 526be1c2e1aec37df13619f06196c53912d97f82 (patch) | |
| tree | a2e3b5b5842f548567c4daebbe8fd9c9bce0dec6 | |
| parent | 068284d23c4a05c7ffeb4db8e277d24ed561369f (diff) | |
update search pattern
fixes #608
| -rw-r--r-- | CONTRIBUTING.md | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 26baba2..15d9ad7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -160,7 +160,8 @@ Abbreviations are in the header of the file which introduces them. We list here - For the infix membership predicate `_ \in _`, the prefix `in_` is used for lemmas that unfold specific predicates, possibly propagating the infix membership (e.g, `in_cons` or `in_set0`). These lemmas are generally part of the `inE` multirule. Other lemmas involving the infix membership predicated use the generic prefix `mem_` (e.g., `mem_head` or `mem_map`). #### Typical search pattern -`Search _ "prefix" "suffix"* (symbol|pattern)* in library.` +- `Search _ "prefix" "suffix"* (symbol|pattern)* in library.` (for coq < 8.12) +- `Search "prefix" "suffix"* (symbol|pattern)* inside library.` (for coq >= 8.12) ### Naming conventions for definitions (non exhaustive) |