CGLocateInductive patched

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index aba3bb3d4e85846ec70f31f2ca1725713cb48627..edf714b1e6a1ecb0e6f2216079182d68d84a6617 100644 (file)
--- a/helm/mathql_test/mqgtop.ml
+++ b/helm/mathql_test/mqgtop.ml
@@ -232,7 +232,7 @@ let mbackward n m l =
 
 let inductive l = 
    let queries = ref [] in
-   let univ = Some C3.universe in 
+   let univ = None in 
    let handle = get_handle () in
    let rec aux = function
       | []           -> ()

diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend
index ef727f7b997c1c1a5fed742d6f4871ccb7ab5287..820add841dc7b55b383bc1f14163acb24296d003 100644 (file)
--- a/helm/ocaml/mathql_generator/.depend
+++ b/helm/ocaml/mathql_generator/.depend
@@ -11,5 +11,5 @@ cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi
 cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi 
 cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi 
 cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi 
-cGLocateInductive.cmo: cGSearchPattern.cmi mQGTypes.cmo cGLocateInductive.cmi 
-cGLocateInductive.cmx: cGSearchPattern.cmx mQGTypes.cmx cGLocateInductive.cmi 
+cGLocateInductive.cmo: mQGTypes.cmo cGLocateInductive.cmi 
+cGLocateInductive.cmx: mQGTypes.cmx cGLocateInductive.cmi 

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml
index 04a2f2ad4806f016479dcceb1cafa81d7ceebb75..032060fd3d7d4736f1696188c7cd367a2527911e 100644 (file)
--- a/helm/ocaml/mathql_generator/cGLocateInductive.ml
+++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml
@@ -38,5 +38,3 @@ let get_constraints = function
       let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in
       (constr_obj, constr_rel, constr_sort)
    | _                      -> raise NotAnInductiveDefinition
-
-let universe = CGSearchPattern.universe 

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.mli b/helm/ocaml/mathql_generator/cGLocateInductive.mli
index e4c6c1fa93badca714d4960f8d304269d22c191d..b6a51401e0805d16cad1a9ea6d1794b9396aa6bf 100644 (file)
--- a/helm/ocaml/mathql_generator/cGLocateInductive.mli
+++ b/helm/ocaml/mathql_generator/cGLocateInductive.mli
@@ -28,6 +28,4 @@
 
 val get_constraints : Cic.term -> MQGTypes.must_restrictions
 
-val universe        : MQGTypes.universe
-
 exception NotAnInductiveDefinition

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 ;