removed dependency on netclient, use http_client module from ocaml-http

[helm.git] / helm / ocaml / mathql_generator / cGMatchConclusion.ml

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 9f1f6451218ca6ab4a92f65d949ee3859ced4f5b..bb87b461efcf548cb7fe1749043c47d0ca5abc4b 100644 (file)
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -26,6 +26,8 @@
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
+module T = MQGTypes
+
 let text_of_entries out entries =
    out "(** MatchConclusion: results of the term inspection **)\n";
    let text_of_entry (u, b, v) =
@@ -41,7 +43,7 @@ let sort_entries entries =
 let levels_of_term metasenv context term =
    let module TC = CicTypeChecker in
    let module Red = CicReduction in
-   let module Util = MQueryUtil in
+   let module Misc = MQueryMisc in
    let degree t =
       let rec degree_aux = function
          | Cic.Sort _         -> 1 
@@ -62,7 +64,7 @@ let levels_of_term metasenv context term =
    in
    let inspect_uri main l uri tc v term =
       let d = degree term in 
-      entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
+      entry_in (Misc.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
    in
    let rec inspect_term main l v term = match term with
         Cic.Rel _                        -> l
@@ -151,17 +153,5 @@ let get_constraints e c t =
         mk_musts (prev @ [acc]) acc next
    in
    mk_musts [] [] can   
-(*
-  let uri_pos (u,b,v) = (u,b) in
-  let can_use = List.map uri_pos can in
-  let lofl (u,b,v) = [(u,b)] in
-  let rec organize_restr rlist prev_r= 
-    match rlist with
-      [] -> []
-    | r::tl ->let curr_r = r@prev_r in
-                curr_r::(organize_restr tl curr_r)
-  in
-  let mrest = List.map lofl can in
-  let must_use = organize_restr mrest [] in (* must restrictions *)
-  (must_use,can_use)
-*)
+
+let universe = [T.MainConclusion; T.InConclusion]