X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=c4dd944b4b956c65479adc70e7d424ae220638a5;hb=c5bbe2a9b9b914f538ae03526c34f2dea5364b1d;hp=e6cbbf692be37411ab8c1ee8c1f10e465179cae6;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index e6cbbf692..c4dd944b4 100644 --- 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 @@ -405,6 +405,12 @@ let render ids_to_uris ?(prec=(-1)) = box_of mathonly (A.H, false, false) attrs (aux_children mathonly false xref prec (CicNotationUtil.ungroup terms))) + | A.Mpadded (l,terms) -> + Mpres.Mpadded + (List.map (fun (k,v) -> None,k,v) l, + box_of mathonly (A.H, false, false) attrs + (aux_children mathonly false xref prec + (CicNotationUtil.ungroup terms))) | A.Group terms -> let children = aux_children mathonly false xref prec