diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-10 19:12:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 15:13:25 -0400 |
| commit | 5f3d20dc53ffd0537a84c93acd761c3c69081342 (patch) | |
| tree | b82efa45c4430b08562b91cf028edef17b97fe34 /theories | |
| parent | 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 (diff) | |
Add transparent_abstract tactic
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_". |