aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacexpr.ml')
-rw-r--r--toplevel/vernacexpr.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d8084c966..e7a66203c 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -69,12 +69,12 @@ type printable =
| PrintAssumptions of reference
type search_about_item =
- | SearchRef of reference
+ | SearchSubPattern of constr_pattern_expr
| SearchString of string * scope_name option
type searchable =
- | SearchPattern of pattern_expr
- | SearchRewrite of pattern_expr
+ | SearchPattern of constr_pattern_expr
+ | SearchRewrite of constr_pattern_expr
| SearchHead of reference
| SearchAbout of (bool * search_about_item) list