]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
parser and pretty printer corrected and tested
[helm.git] / helm / ocaml / mathql / mathQL.ml
index ed6abf54f454c0b6b6c32afd5d9b6858a5fe5059..b424d110b56bc8247b6fa8b750487668bf603842 100644 (file)
@@ -58,7 +58,8 @@ type set_exp = SVar of svar
             | Union of set_exp * set_exp
             | Intersect of set_exp * set_exp
             | Diff of set_exp * set_exp
-            | Let of svar * set_exp * set_exp
+            | LetSVar of svar * set_exp * set_exp
+            | LetVVar of vvar * val_exp * set_exp
             
 and boole_exp = False
               | True
@@ -73,6 +74,7 @@ and boole_exp = False
 and val_exp = Const of string list 
             | RefOf of set_exp 
            | Record of rvar * vvar
+           | VVar of vvar
            | Fun of string * val_exp
            | Attribute of refine_op * string * val_exp