From: Ferruccio Guidi Date: Fri, 7 Nov 2003 11:48:13 +0000 (+0000) Subject: new Gen constructor for interfacing a query generator X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=605740107642920d90d0c88544d576d7836a1a25 new Gen constructor for interfacing a query generator --- diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 9c19f4a50..884976fe5 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -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 *