X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=305fe57947edba39d50e13c0c834230b1e15a023;hb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;hp=04440ffe7a75cefe1ce1b7d9315f2ef197928611;hpb=fb9f80d2fb30216cc0754e8e8d09206f3e3e7bb7;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 04440ffe7..305fe5794 100644
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -262,32 +262,12 @@ let render status ~lookup_uri ?(prec=(-1)) =
           @ make_href xmlattrs xref
         in
         Mpres.Mo (attrs, to_unicode literal)
-    | A.Ident (literal, subst)
-    | A.Uri (literal, subst) ->
+    | A.Ident (literal, _) ->
         let attrs =
           (RenderingAttrs.ident_attributes `MathML)
           @ make_href xmlattrs xref
         in
-        let name = Mpres.Mi (attrs, to_unicode literal) in
-        (match subst with
-        | Some []
-        | None -> name
-        | Some substs ->
-            let substs' =
-              box_of mathonly (A.H, false, false) []
-                (open_brace
-                :: (NotationUtil.dress semicolon
-                    (List.map
-                      (fun (name, t) ->
-                        box_of mathonly (A.H, false, false) [] [
-                          Mpres.Mi ([], name);
-                          Mpres.Mo ([], to_unicode "\\def");
-                          aux [] mathonly xref  prec t ])
-                      substs))
-                @ [ closed_brace ])
-            in
-            let substs_maction = toggle_action [ hidden_substs; substs' ] in
-            box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
+        Mpres.Mi (attrs, to_unicode literal)
     | A.Meta(n, l) ->
         let local_context l =
           box_of mathonly (A.H, false, false) []