X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fxoa%2Fengine.ml;h=fa4bb7ff6ef38591463852475eefc8838b22bcde;hb=127be10fa95b5b347887241e046d72e432944e61;hp=d650f07b518dee5507fe4d6616315061cb8761d6;hpb=81cf2dd18ed76a214ab610447d0c5861998b3d96;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