]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/content.mli
fixed some TODO in content2pres
[helm.git] / helm / ocaml / cic_omdoc / content.mli
index 9a38ea4be5578d5c1a06fd2dac47d74c94272401..99869b9b47623ab226574da143eb625ec3e5bdfe 100644 (file)
@@ -100,7 +100,7 @@ type 'term proof =
 
 and 'term in_proof_context_element =
        [ 'term decl_context_element
-       | ('term,'term proof) def_context_element
+       | ('term,'term proof) def_context_element 
        | ('term,'term proof) joint_context_element
        ]