]> matita.cs.unibo.it Git - helm.git/commitdiff
new Gen constructor for interfacing a query generator
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 7 Nov 2003 11:48:13 +0000 (11:48 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 7 Nov 2003 11:48:13 +0000 (11:48 +0000)
helm/ocaml/mathql/mathQL.ml

index 9c19f4a50f325fdab3648f531518dd29c785576c..884976fe575e514d8c4f4cd93fd83e77e7ba39c4 100644 (file)
@@ -82,6 +82,7 @@ type query = Const of result
           | Select of avar * query * query
           | Let of svar * 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
           | Property of inverse * refine * path *