X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQGUtil.mli;h=065abb1573a30b3015c234cd5ebb0860c5557127;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bb623cc86c74ddb4b5e4a9966375e36c41a30d24;hpb=0e74e8e94eada756157addce67e4adeb8dff1feb;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQGUtil.mli b/helm/ocaml/mathql_generator/mQGUtil.mli
index bb623cc86..065abb157 100644
--- a/helm/ocaml/mathql_generator/mQGUtil.mli
+++ b/helm/ocaml/mathql_generator/mQGUtil.mli
@@ -67,8 +67,3 @@ val set_full_position : MQGTypes.full_position -> MQGTypes.optional_depth ->
                         MQGTypes.full_position
 val set_main_position : MQGTypes.main_position -> MQGTypes.optional_depth ->
                         MQGTypes.main_position
-
-(* these functions give some universes for "query_of_constraints"  ---------*)
-
-val universe_for_search_pattern   : MQGTypes.universe
-val universe_for_match_conclusion : MQGTypes.universe