Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / cic_transformations / sequentPp.ml

diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml
index bda66841cc2cfd82bbda49aa80a24694dcfd3eb0..e7b3151ea02ef7d9f4863155fe493c632d7f6a35 100644 (file)
--- 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