]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
while construction inserted
[helm.git] / helm / ocaml / mathql / mathQL.ml
index 884976fe575e514d8c4f4cd93fd83e77e7ba39c4..8ba562ab210648bea3c44a2c8cce9b9fd883093c 100644 (file)
@@ -80,11 +80,12 @@ type query = Const of result
           | Dot of avar * path
           | Ex of avar list * query
           | Select of avar * query * query
-          | Let of svar * query * query
+          | Let of svar option * query * query
           | Fun of path * path list * query list
           | Gen of path * query list
           | Add of bool * groups * query
           | For of gen * avar * query * query
+          | While of gen * query * query
           | Property of inverse * refine * path * 
                         main * istrue * isfalse list * exp_list *
                         pattern * query