X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=82a326c48bbb4ffc70d64400ef043b1b74955fa0;hb=HEAD;hp=35f128a05b524078b117a394cb51b87a8554f6d1;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 35f128a05..82a326c48 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -371,6 +371,9 @@ let render ~lookup_uri ?(prec=(-1)) = (* use the one below to reset precedence and associativity *) let invoke_reinit t = aux [] mathonly xref ~-1 t in match l with + | A.Sup (A.Layout (A.Sub (t1,t2)), t3) + | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3) + -> Mpres.Msubsup (attrs, invoke' t1, invoke_reinit t2, invoke_reinit t3) | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2) | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2) | A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2)