From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 4 Sep 2003 13:07:26 +0000 (+0000)
Subject: CGLocateInductive patched
X-Git-Tag: v0_0_1~53
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=36d9dada5eb3894d96c807781e1056b73a1c0a79

CGLocateInductive patched
---

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index aba3bb3d4..edf714b1e 100644
--- 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 ef727f7b9..820add841 100644
--- 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 04a2f2ad4..032060fd3 100644
--- 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 e4c6c1fa9..b6a51401e 100644
--- 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 622f10bd5..f7fae9481 100644
--- 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 ;