X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FsequentPp.ml;h=e7b3151ea02ef7d9f4863155fe493c632d7f6a35;hb=fde0ad77237a2fbdfb5621d5b5085fe7c82e3f92;hp=8cce6e1e39a116e8200bed2a35f2dc339e8841be;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml
index 8cce6e1e3..e7b3151ea 100644
--- a/helm/ocaml/cic_transformations/sequentPp.ml
+++ b/helm/ocaml/cic_transformations/sequentPp.ml
@@ -38,10 +38,11 @@ module TextualPp =
          match i with
             Some (n,Cic.Decl t) ->
               print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
-          | Some (n,Cic.Def t) ->
+          | Some (n,Cic.Def (t,None)) ->
               print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
           | None ->
               "_ ?= _\n", None::context
+          | Some (_,Cic.Def (_,Some _)) -> assert false
         in
          output^newoutput,context'
       ) ctx ("",[])
@@ -84,26 +85,28 @@ module XmlPp =
             Hashtbl.add ids_to_hypotheses hid binding ;
             incr hypotheses_seed ;
             match binding with
-               (Some (n,(Cic.Def t as b)) as entry)
+               (Some (n,(Cic.Def (t,None) as b)) as entry)
              | (Some (n,(Cic.Decl t as b)) as entry) ->
                 let acic = acic_of_cic_context context idrefs t None in
                  [< s ;
                     X.xml_nempty
                      (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
-                     ["name",(match n with Cic.Name n -> n | _ -> assert false);
-                      "id",hid]
+                     [None,"name",(match n with Cic.Name n -> n | _ -> assert false);
+                      None,"id",hid]
                      (Cic2Xml.print_term ~ids_to_inner_sorts acic)
                  >], (entry::context), (hid::idrefs)
              | None ->
                 (* Invariant: "" is never looked up *)
                 [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+             | Some (_,Cic.Def (_,Some _)) -> assert false
          ) context ([<>],[],[])
        )
       in
        let acic = acic_of_cic_context context final_idrefs goal None in
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
             X.xml_cdata ("<!DOCTYPE Sequent SYSTEM \"" ^ dtdname ^ "\">\n");
-            X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id]
+            X.xml_nempty "Sequent"
+             [None,"no",string_of_int metano;None,"id",sequent_id]
              [< final_s ;
                 Xml.xml_nempty "Goal" []
                  (Cic2Xml.print_term ~ids_to_inner_sorts acic)