xoa: change in naming convenctions for existential quantifies

[helm.git] / matita / components / binaries / xoa / engine.ml

diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml
index d650f07b518dee5507fe4d6616315061cb8761d6..fa4bb7ff6ef38591463852475eefc8838b22bcde 100644 (file)
--- 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