natural deduction support for lemmas with premises

[helm.git] / helm / software / components / content_pres / cicNotationPres.ml

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index e6cbbf692be37411ab8c1ee8c1f10e465179cae6..77dc2b08cf8c52ebfcf2fb7f49b8e98f2eaa6903 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -331,7 +331,7 @@ let render ids_to_uris ?(prec=(-1)) =
           | `Raw _ -> ()
           | `Level (-1) -> reset := true
           | `Level child_prec ->
-              assert (!expected_level = None);
+(*               assert (!expected_level = None); *)
               expected_level := !inferred_level;
               inferred_level := Some child_prec
           | `IdRef xref -> new_xref := xref :: !new_xref