X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate2%2Fmk_forward%2Fmk_forward.ml;h=e97ed33476e05b2c3e7072e2fca30a39dd1a89c1;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=2947461242f07439490a855dd3604c25a3aba1ac;hpb=a12fefc78e783661fbb638907252d2265c6af9dd;p=helm.git diff --git a/helm/metadata/create2/mk_forward/mk_forward.ml b/helm/metadata/create2/mk_forward/mk_forward.ml index 294746124..e97ed3347 100644 --- 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/" ^