Now MQueryGenerator generates the query and MQueryLevels produces the restrictions...

[helm.git] / helm / ocaml / cic / cicParser2.ml

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index e74cf73d35924d83f0650a79d8976b23cf1d0241..15bc2b9350f88f090cc2a538c06bf78c8cd0e128 100644 (file)
--- 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)