aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/dune1
-rw-r--r--theories/ssrsearch/ssrsearch.v2
2 files changed, 3 insertions, 0 deletions
diff --git a/theories/dune b/theories/dune
index b9af76d699..de8dcdc5b1 100644
--- a/theories/dune
+++ b/theories/dune
@@ -33,6 +33,7 @@
coq.plugins.funind
coq.plugins.ssreflect
+ coq.plugins.ssrsearch
coq.plugins.derive))
(include_subdirs qualified)
diff --git a/theories/ssrsearch/ssrsearch.v b/theories/ssrsearch/ssrsearch.v
new file mode 100644
index 0000000000..37ab8f4bac
--- /dev/null
+++ b/theories/ssrsearch/ssrsearch.v
@@ -0,0 +1,2 @@
+Require Import ssreflect.
+Declare ML Module "ssrsearch_plugin".