X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fxoa%2Fengine.ml;h=fa4bb7ff6ef38591463852475eefc8838b22bcde;hb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;hp=d650f07b518dee5507fe4d6616315061cb8761d6;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml
index d650f07b5..fa4bb7ff6 100644
--- a/matita/components/binaries/xoa/engine.ml
+++ b/matita/components/binaries/xoa/engine.ml
@@ -31,7 +31,9 @@ let void_iter f n =
 let mk_exists ooch noch c v =
    let description = "multiple existental quantifier" in
    let prec = "non associative with precedence 20\n" in
-   let name s = P.sprintf "%s%u_%u" s c v in
+   let name s = 
+      if v = 1 then P.sprintf "%s%u" s c else P.sprintf "%s%u_%u" s c v
+   in
    let o_name = name "ex" in
    let i_name = "'Ex" in