diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:06:47 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:06:47 +0200 |
| commit | e302b4dbc88c5776155c770aa90134edb571b738 (patch) | |
| tree | cbb6d8a40f7e1baa30ce4968589b82b90b63b891 /theories | |
| parent | a1788978360bd276bef721963e7adc47c1a49881 (diff) | |
| parent | e4262a89d7bc3d9b985d9a4a939f34176581abcb (diff) | |
Merge PR#201: Transparent abstract
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Prelude.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index c58d23dad..e71a8774e 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -23,4 +23,4 @@ Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". (* Default substrings not considered by queries like SearchAbout *) -Add Search Blacklist "_subproof" "Private_". +Add Search Blacklist "_subproof" "_subterm" "Private_". |