X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fmathql%2FmathQL.ml;h=d18ebbc9243afa5d1fc3b87e8718cc68aaf83116;hb=1d2bd140d14561951f8214edf15abe4f40dcb649;hp=90d17c553a76f3cc7e8b93c1a6ffde6ff2a76b8b;hpb=8adca9e9d6f3b7c605e570dadb4bb82a16b3d050;p=helm.git

diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml
index 90d17c553..d18ebbc92 100644
--- a/helm/ocaml/mathql/mathQL.ml
+++ b/helm/ocaml/mathql/mathQL.ml
@@ -67,8 +67,6 @@ type mquref = UriManager.uri * (int list) (* uri, fragment identifier *)
 
 type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized pattern reference *)
 
-type mqref = string (* format for references (helper) *)
-
 type mqfunc =
    | MQName         (* Name *)
    | MQTheory       (* theory *)
@@ -115,7 +113,7 @@ type mqbool =
    | MQSubset of mqlist * mqlist   (* the two lists denote two sets, the 1st subset of the 2nd *)
 
 and mqlist =
-   | MQReference of mqref                    (* reference *)
+   | MQReference of string list              (* reference list *)
    | MQPattern of mqtref                     (* pattern *)
    | MQListLVar of mqlvar                    (* lvar *)
    | MQListRVar of mqrvar                    (* rvar *)
@@ -127,8 +125,7 @@ and mqlist =
    | MQSortedBy of mqlist * mqorder * mqfunc (* ordering *)
    | MQDiff of mqlist * mqlist               (* set difference  *)
    | MQLetIn of mqlvar * mqlist * mqlist     (* explicit lvar assignment *)
-   | MQMinimize of mqlist                    (* list minimization *)
-   
+
 type mquery =
    | MQList of mqlist
    
@@ -136,4 +133,4 @@ type mquery =
 (* main type is mqresult                                                    *)
 
 type mqresult =
-   | MQRefs of mqref list
+   | MQRefs of string list