aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/search.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/search.mli')
-rw-r--r--vernac/search.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/search.mli b/vernac/search.mli
index c9167c485..82b79f75d 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -67,7 +67,7 @@ type 'a coq_object = {
}
val interface_search : ?glnum:int -> (search_constraint * bool) list ->
- string coq_object list
+ constr coq_object list
(** {6 Generic search function} *)