CGLocateInductive patched

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

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 622f10bd5a618979fcf19551b1c32a659536cd99..f7fae9481e6d0ac093705fa5fd21f7f50fba5dd7 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -178,20 +178,20 @@ let contype = "Content-Type", "text/html";;
 let get_constraints term =
  function
     | "/locateInductivePrinciple" ->
-      CGLocateInductive.universe,
+      None,
       (CGLocateInductive.get_constraints term),
       (None,None,None)
     | "/searchPattern" ->
      let constr_obj, constr_rel, constr_sort =
        CGSearchPattern.get_constraints term in
-      CGSearchPattern.universe,
-       (constr_obj, constr_rel, constr_sort),
-       (Some constr_obj, Some constr_rel, Some constr_sort)
+     (Some CGSearchPattern.universe),
+     (constr_obj, constr_rel, constr_sort),
+     (Some constr_obj, Some constr_rel, Some constr_sort)
     | "/matchConclusion" ->
      let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
 (* FG: there is no way to choose the block number ***************************)
      let block = pred (List.length list_of_must) in 
-      CGMatchConclusion.universe, 
+      (Some CGMatchConclusion.universe), 
       (List.nth list_of_must block, [], []), (Some only, None, None)
     | _ -> assert false
 ;;
@@ -579,7 +579,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                   raise Chat_unfinished)
             in
             let query =
-             G.query_of_constraints (Some universe) must'' only'
+             G.query_of_constraints universe must'' only'
             in
                  let results = MQueryInterpreter.execute mqi_handle query in 
              Http_daemon.send_basic_headers ~code:200 outchan ;