ocaml 3.09 transition

[helm.git] / helm / fix_params / cic2Xml.ml

diff --git a/helm/fix_params/cic2Xml.ml b/helm/fix_params/cic2Xml.ml
index 58f35bb6f687c0581bd611589ac9ee94f3e25d97..0d433d64add316b6cbf16bde494f8ec8e93a3be6 100644 (file)
--- a/helm/fix_params/cic2Xml.ml
+++ b/helm/fix_params/cic2Xml.ml
@@ -28,8 +28,6 @@
 
 exception ImpossiblePossible;;
 exception NotImplemented;;
-exception BinderNotSpecified;;
-
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
@@ -39,19 +37,18 @@ let print_term curi =
   let module X = Xml in
   let module U = UriManager in
     function
-       C.ARel (id,_,n,Some b) ->
+       C.ARel (id,n,b) ->
         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
-     | C.ARel _ -> raise BinderNotSpecified
-     | C.AVar (id,_,uri) ->
+     | C.AVar (id,uri) ->
         let vdepth = U.depth_of_uri uri
         and cdepth = U.depth_of_uri curi in
          X.xml_empty "VAR"
           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
             (U.name_of_uri uri) ;
            "id",id]
-     | C.AMeta (id,_,n) ->
+     | C.AMeta (id,n) ->
         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
-     | C.ASort (id,_,s) ->
+     | C.ASort (id,s) ->
         let string_of_sort =
          function
             C.Prop -> "Prop"
@@ -60,56 +57,55 @@ let print_term curi =
         in
          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
      | C.AImplicit _ -> raise NotImplemented
-     | C.AProd (id,_,C.Anonimous,s,t) ->
+     | C.AProd (id,C.Anonimous,s,t) ->
         X.xml_nempty "PROD" ["id",id]
          [< X.xml_nempty "source" [] (aux s) ;
             X.xml_nempty "target" [] (aux t)
          >]
-     | C.AProd (xid,_,C.Name id,s,t) ->
+     | C.AProd (xid,C.Name id,s,t) ->
        X.xml_nempty "PROD" ["id",xid]
         [< X.xml_nempty "source" [] (aux s) ;
            X.xml_nempty "target" ["binder",id] (aux t)
         >]
-     | C.ACast (id,_,v,t) ->
+     | C.ACast (id,v,t) ->
         X.xml_nempty "CAST" ["id",id]
          [< X.xml_nempty "term" [] (aux v) ;
             X.xml_nempty "type" [] (aux t)
          >]
-     | C.ALambda (id,_,C.Anonimous,s,t) ->
+     | C.ALambda (id,C.Anonimous,s,t) ->
         X.xml_nempty "LAMBDA" ["id",id]
          [< X.xml_nempty "source" [] (aux s) ;
             X.xml_nempty "target" [] (aux t)
          >]
-     | C.ALambda (xid,_,C.Name id,s,t) ->
+     | C.ALambda (xid,C.Name id,s,t) ->
        X.xml_nempty "LAMBDA" ["id",xid]
         [< X.xml_nempty "source" [] (aux s) ;
            X.xml_nempty "target" ["binder",id] (aux t)
         >]
-     | C.ALetIn (xid,_,C.Anonimous,s,t) ->
+     | C.ALetIn (xid,C.Anonimous,s,t) ->
        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
-     | C.ALetIn (xid,_,C.Name id,s,t) ->
+     | C.ALetIn (xid,C.Name id,s,t) ->
        X.xml_nempty "LETIN" ["id",xid]
         [< X.xml_nempty "term" [] (aux s) ;
            X.xml_nempty "letintarget" ["binder",id] (aux t)
         >]
-     | C.AAppl (id,_,li) ->
+     | C.AAppl (id,li) ->
         X.xml_nempty "APPLY" ["id",id]
          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
          >]
-     | C.AConst (id,_,uri,_) ->
+     | C.AConst (id,uri,_) ->
         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
-     | C.AAbst (id,_,uri) -> raise NotImplemented
-     | C.AMutInd (id,_,uri,_,i) ->
+     | C.AMutInd (id,uri,_,i) ->
         X.xml_empty "MUTIND"
          ["uri", (U.string_of_uri uri) ;
           "noType",(string_of_int i) ;
           "id",id]
-     | C.AMutConstruct (id,_,uri,_,i,j) ->
+     | C.AMutConstruct (id,uri,_,i,j) ->
         X.xml_empty "MUTCONSTRUCT"
          ["uri", (U.string_of_uri uri) ;
           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
           "id",id]
-     | C.AMutCase (id,_,uri,_,typeno,ty,te,patterns) ->
+     | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
         X.xml_nempty "MUTCASE"
          ["uriType",(U.string_of_uri uri) ;
           "noType", (string_of_int typeno) ;
@@ -120,7 +116,7 @@ let print_term curi =
              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
              patterns [<>]
          >]
-     | C.AFix (id, _, no, funs) ->
+     | C.AFix (id, no, funs) ->
        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
         [< List.fold_right
             (fun (fi,ai,ti,bi) i ->
@@ -133,7 +129,7 @@ let print_term curi =
               >]
             ) funs [<>]
         >]
-     | C.ACoFix (id,_,no,funs) ->
+     | C.ACoFix (id,no,funs) ->
        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
         [< List.fold_right
             (fun (fi,ti,bi) i ->
@@ -186,7 +182,7 @@ let pp obj curi =
  let module C = Cic in
  let module X = Xml in
   match obj with
-     C.ADefinition (xid, _, id, te, ty, params) ->
+     C.ADefinition (xid, id, te, ty, params) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
          X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
          X.xml_nempty "Definition"
@@ -199,7 +195,7 @@ let pp obj curi =
           [< X.xml_nempty "body" [] (print_term curi te) ;
              X.xml_nempty "type"  [] (print_term curi ty) >]
       >]
-   | C.AAxiom (xid, _, id, ty, params) ->
+   | C.AAxiom (xid, id, ty, params) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
          X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
          X.xml_nempty "Axiom"
@@ -208,7 +204,7 @@ let pp obj curi =
           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
           [< X.xml_nempty "type" [] (print_term curi ty) >]
       >]
-   | C.AVariable (xid, _, name, bo, ty) ->
+   | C.AVariable (xid, name, bo, ty) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
          X.xml_nempty "Variable" ["name",name ; "id",xid]
@@ -219,7 +215,7 @@ let pp obj curi =
              X.xml_nempty "type" [] (print_term curi ty)
           >]
       >]
-   | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
+   | C.ACurrentProof (xid, name, conjs, bo, ty) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
          X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
          X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
@@ -232,7 +228,7 @@ let pp obj curi =
              X.xml_nempty "type" [] [< print_term curi ty >]
           >]
       >]
-   | C.AInductiveDefinition (xid, _, tys, params, paramsno) ->
+   | C.AInductiveDefinition (xid, tys, params, paramsno) ->
       let names =
        List.map
         (fun (typename,_,_,_) -> typename)