]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/xoa/ast.ml
the generation of the multiple conjunction is now supported!
[helm.git] / matita / components / binaries / xoa / ast.ml
index 4de0c10579e07b5c66947796eeef8a23983f3325..42285524036073349c2ba7c1c67c93bba14304c7 100644 (file)
@@ -15,7 +15,10 @@ type subarity = int
 
 type directive = Exists of arity * subarity
                | Or of arity
+               | And of arity
 
 let mk_exists c v = Exists (c, v)
 
 let mk_or c = Or c 
+
+let mk_and c = And c