X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=c4dd944b4b956c65479adc70e7d424ae220638a5;hb=dba85ad7c7510e7bfd01e5721c63dad528b3e0bf;hp=77dc2b08cf8c52ebfcf2fb7f49b8e98f2eaa6903;hpb=404cfbb5d450f3d738637cfee71aac877a4a8b1d;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 77dc2b08c..c4dd944b4 100644
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -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