X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser2.ml;h=15bc2b9350f88f090cc2a538c06bf78c8cd0e128;hb=8b9c9eae1f9da8908ede64b37f04bb7d9e476f7a;hp=e74cf73d35924d83f0650a79d8976b23cf1d0241;hpb=08a2b1a3f1a1e9af07850089f0e0838eb052223d;p=helm.git

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index e74cf73d3..15bc2b935 100644
--- a/helm/ocaml/cic/cicParser2.ml
+++ b/helm/ocaml/cic/cicParser2.ml
@@ -163,10 +163,11 @@ let rec get_inductive_types =
   | he::tl ->
      let tyname    = string_of_attr (he#attribute "name")
      and inductive = bool_of_attr   (he#attribute "inductive")
+     and xid = string_of_attr (he#attribute "id")
      and (arity,cons) =
       get_names_arity_constructors (he#sub_nodes)
      in
-      (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
+      (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
 ;;
 
 (* This is the main function and also the only one used directly from *)
@@ -194,26 +195,24 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
             let nbodytype = nbody'#node_type in
             match nbodytype with
              D.T_element "ConstantBody" ->
+(*CSC: the attribute "for" is ignored and not checked
               let for_ = string_of_attr (nbody'#attribute "for") in
+*)
               let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
               let xidbody = string_of_attr (nbody'#attribute "id") in
               let value = (get_content nbody')#extension#to_cic_term [] in
-               if paramsbody = params &&
-                  U.eq (U.uri_of_string for_) !CicParser3.current_uri
-               then
+               if paramsbody = params then
                 C.AConstant (xid, Some xidbody, name, Some value, typ, params)
                else
                 raise (IllFormedXml 6)
            | D.T_element "CurrentProof" ->
+(*CSC: the attribute "of" is ignored and not checked
               let for_ = string_of_attr (nbody'#attribute "of") in
+*)
               let xidbody = string_of_attr (nbody'#attribute "id") in
-              let value = (get_content nbody')#extension#to_cic_term [] in
               let sons = nbody'#sub_nodes in
                let (conjs, value) = get_conjs_value sons in
-                if U.eq (U.uri_of_string for_) !CicParser3.current_uri then
-                 C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
-                else
-                 raise (IllFormedXml 6)
+                C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
            | D.T_element _
            | D.T_data
            | _ -> raise (IllFormedXml 6)