From: Ferruccio Guidi Date: Tue, 21 May 2002 15:24:24 +0000 (+0000) Subject: MQRefs fixed X-Git-Tag: V_0_3_0_debian_8~89 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8caa5383c2ef78e8516881b1e7161f71f8ddca40;p=helm.git MQRefs fixed --- diff --git a/helm/ocaml/mathql_interpreter/mathql.ml b/helm/ocaml/mathql_interpreter/mathql.ml index 1fea24c2e..2bdc5a1b7 100644 --- a/helm/ocaml/mathql_interpreter/mathql.ml +++ b/helm/ocaml/mathql_interpreter/mathql.ml @@ -99,8 +99,7 @@ type mquery = (* TODO: usare le uri in questo formato *) type mquref = UriManager.uri * mqfi (* uri, fragment identifier *) -type mqrefs = mqtref list (* list of references (helper) *) +type mqrefs = string list (* list of references (helper) *) -type mqresult = - | MQStrUri of string list +type mqresult = | MQRefs of mqrefs diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index 62c12d441..240881771 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -72,7 +72,7 @@ let rec execute_ex q = * la uri puo' far parte del risultato. *) let xres_to_res l = - MQStrUri + MQRefs ( List.map List.hd