Tracing mechanism for auto. Interface changed to solve an ambiguity between

[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 35f128a05b524078b117a394cb51b87a8554f6d1..82a326c48bbb4ffc70d64400ef043b1b74955fa0 100644 (file)
--- 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)