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

diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml
index bda66841c..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,7 +85,7 @@ 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 ;
@@ -97,6 +98,7 @@ module XmlPp =
              | None ->
                 (* Invariant: "" is never looked up *)
                 [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+             | Some (_,Cic.Def (_,Some _)) -> assert false
          ) context ([<>],[],[])
        )
       in