aboutsummaryrefslogtreecommitdiff
path: root/vernac/search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/search.ml')
-rw-r--r--vernac/search.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/search.ml b/vernac/search.ml
index 1fac28358a..6610789626 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -172,8 +172,8 @@ let prioritize_search seq fn =
(** Filters *)
-(** This function tries to see whether the conclusion matches a pattern. *)
-(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
+(** This function tries to see whether the conclusion matches a pattern.
+ FIXME: this is quite dummy, we may find a more efficient algorithm. *)
let rec pattern_filter pat ref env sigma typ =
let typ = Termops.strip_outer_cast sigma typ in
if Constr_matching.is_matching env sigma pat typ then true