]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/options.ml
level disambiguation cmpleted! the Grafite file is succesfully generated.
[helm.git] / helm / software / helena / src / common / options.ml
index e7666efe3427cb323ec2fd9827d09f1de43100f6..a7b5f4dd599738f584ee35ca512331f2beb27e7b 100644 (file)
@@ -53,6 +53,8 @@ let ma_dir = ref ""          (* directory for grafite output *)
 
 let ma_preamble = ref ""     (* location of grafite preamble file *)
 
+let alpha = ref ""           (* prefix of numeric identifiers *)
+
 let kernel_id () = 
    let id = match !kernel with
       | Crg -> "crg"