X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;h=353ef1f7496082b445329372061f59c56ce83d06;hb=b266dce15b2f669a70daaee3bd0887f8d9c345b2;hp=7ea0b7b6309937574d1cae19e93d9345928aed46;hpb=b57c31a1593872c181249135bc05ebd9a72f523b;p=helm.git

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 7ea0b7b63..353ef1f74 100644
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -50,8 +50,7 @@ let print_term i2a =
   let module X = Xml in
   let module U = UriManager in
     function
-       C.ARel (id,_,_) -> print_ann i2a id
-     | C.AVar (id,_) -> print_ann i2a id
+       C.ARel (id,_,_,_) -> print_ann i2a id
      | C.AMeta (id,_,_) -> print_ann i2a id
      | C.ASort (id,_) -> print_ann i2a id
      | C.AImplicit _ -> raise NotImplemented
@@ -63,11 +62,16 @@ let print_term i2a =
         [< print_ann i2a id ;
            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
         >]
-     | C.AConst (id,_,_) -> print_ann i2a id
-     | C.AAbst (id,_) -> raise NotImplemented
-     | C.AMutInd (id,_,_,_) -> print_ann i2a id
-     | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
-     | C.AMutCase (id,_,_,_,ty,te,patterns) ->
+     | C.AVar (id,_,exp_named_subst)
+     | C.AConst (id,_,exp_named_subst)
+     | C.AMutInd (id,_,_,exp_named_subst)
+     | C.AMutConstruct (id,_,_,_,exp_named_subst) ->
+        [< print_ann i2a id ;
+           List.fold_right
+            (fun (_,x) i -> [< aux x ; i >])
+            exp_named_subst [<>]
+        >] 
+     | C.AMutCase (id,_,_,ty,te,patterns) ->
         [< print_ann i2a id ;
            aux ty ;
            aux te ;
@@ -78,21 +82,21 @@ let print_term i2a =
      | C.AFix (id,_,funs) ->
         [< print_ann i2a id ;
            List.fold_right
-            (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
+            (fun (_,_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
         >]
      | C.ACoFix (id,no,funs) ->
         [< print_ann i2a id ;
            List.fold_right
-            (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
+            (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
         >]
  in
   aux
 ;;
 
-let print_mutual_inductive_type i2a (_,_,arity,constructors) =
+let print_mutual_inductive_type i2a (_,_,_,arity,constructors) =
  [< print_term i2a arity ;
     List.fold_right
-     (fun (name,ty,_) i -> [< print_term i2a ty ; i >]) constructors [<>]
+     (fun (name,ty) i -> [< print_term i2a ty ; i >]) constructors [<>]
  >]
 ;;
 
@@ -105,10 +109,19 @@ let pp_annotation obj i2a curi =
       ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
       begin
        match obj with
-         C.ADefinition (xid, _, te, ty, _) ->
-          [< print_ann i2a xid ; print_term i2a te ; print_term i2a ty >]
-       | C.AAxiom (xid, _, ty, _) -> [< print_ann i2a xid ; print_term i2a ty >]
-       | C.AVariable (xid, _, bo, ty) ->
+         C.AConstant (xid, xidobj, _, te, ty, _) ->
+          [< print_ann i2a xid ;
+             (match xidobj,te with
+                 Some xidobj, Some te ->
+                  [< print_ann i2a xidobj ;
+                     print_term i2a te
+                  >]
+               | None, None -> [<>]
+               | _,_ -> assert false
+             ) ;
+             print_term i2a ty
+          >]
+       | C.AVariable (xid, _, bo, ty,_) ->
           [< print_ann i2a xid ;
              (match bo with
                  None -> [<>]
@@ -116,8 +129,9 @@ let pp_annotation obj i2a curi =
              ) ;
              print_term i2a ty
           >]
-       | C.ACurrentProof (xid, _, conjs, bo, ty) ->
+       | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) ->
           [< print_ann i2a xid ;
+             print_ann i2a xidobj ;
              List.fold_right
               (fun (cid, _, context, t) i ->
                 [< print_ann i2a cid ;