aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-11 17:41:58 +0200
committerThéo Zimmermann2020-05-15 18:05:11 +0200
commit023d189aa201c8d5c71bc7de3e98725273d01b4f (patch)
treefef307bc4bf50447d44a972d53110cee60759192 /doc/stdlib
parent7c113b3a736e8a374b8a57aacde846fc5c5cbf3f (diff)
Move SSR's Search to a new plugin and deprecate it.
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/hidden-files1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 3af16cb731..0a9dba99a9 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -91,3 +91,4 @@ theories/setoid_ring/Rings_Z.v
theories/setoid_ring/ZArithRing.v
theories/ssr/ssrunder.v
theories/ssr/ssrsetoid.v
+theories/ssrsearch/ssrsearch.vo