- some code patched

[helm.git] / helm / searchEngine / searchEngine.ml

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 1762e5fd9f161f4da5409a3526abbdcfd953da66..fc0fb9cbee4ec2af67bb77d7f2b12ccfc1f269c2 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -459,8 +459,8 @@ let callback mqi_handle (req: Http_types.request) outchan =
                   interactive_interpretation_choice_TPL;
                 raise Chat_unfinished
 
-            let input_or_locate_uri ~title =
-              UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
+            let input_or_locate_uri ~title ?id () =
+             assert false
 
           end
         in