mathql_generator: new constraint format (more type safe)

[helm.git] / helm / hbugs / tutors / search_pattern_apply_tutor.ml

diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
index d7b2da2ba04e63357d50f51d1c812b79909e4256..8ba1f8386b7c4846b2b8b4fbb07c2135fab54e2a 100644 (file)
--- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml
+++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
@@ -32,7 +32,7 @@ let slave mqi_handle (state, musing_id) =
         | hd::tl -> hd
       in
       let uris =
-        TacticChaser.searchPattern mqi_handle
+        TacticChaser.matchConclusion mqi_handle
          ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
       in
       if uris = [] then