- the mathql interpreter is not helm-dependent any more

[helm.git] / helm / metadata / create2 / mk_forward / mk_forward.ml

diff --git a/helm/metadata/create2/mk_forward/mk_forward.ml b/helm/metadata/create2/mk_forward/mk_forward.ml
index 2947461242f07439490a855dd3604c25a3aba1ac..e97ed33476e05b2c3e7072e2fca30a39dd1a89c1 100644 (file)
--- a/helm/metadata/create2/mk_forward/mk_forward.ml
+++ b/helm/metadata/create2/mk_forward/mk_forward.ml
@@ -134,7 +134,7 @@ let output_file cic_string_uri rdf_string_uri =
        X.xml_nempty "rdf:RDF"
         ["xml:lang","en" ;
          "xmlns:rdf","http://www.w3.org/1999/02/22-rdf-syntax-ns#";
-         "xmlns:h","http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#"]
+         "xmlns:h","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#"]
 
         (try
           Stream.empty content ; (* raise Stream.failure if not empty *)
@@ -149,12 +149,7 @@ let output_file cic_string_uri rdf_string_uri =
 
 let get_obj uri =
  let cicfilename = Getter.getxml uri in
-  let res =
-   match CicParser.term_of_xml cicfilename uri false with
-      (annobj, None) ->
-        Deannotate.deannotate_obj annobj
-    | _ -> assert false
-  in
+  let res = CicParser.obj_of_xml cicfilename uri in
    Unix.unlink cicfilename ;
    res
 ;;
@@ -212,7 +207,6 @@ let process_type term =
     | C.Appl _ -> assert false
     | C.Const (uri,_) ->
        UriHash.add_uri (U.string_of_uri uri) kind
-    | C.Abst _ -> assert false
     | C.MutInd (uri,_,typeno) ->
        H.add_uri
         (U.string_of_uri uri ^ "#xpointer(1/" ^
@@ -272,7 +266,6 @@ let process_body =
        List.iter process_body_aux l
     | C.Const (uri,_) ->
        UriHash.add_uri (U.string_of_uri uri) H.InBody
-    | C.Abst _ -> assert false
     | C.MutInd (uri,_,typeno) ->
        H.add_uri
         (U.string_of_uri uri ^ "#xpointer(1/" ^