X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_test%2Fmqgtop.ml;h=9e1dcde0d99dba624ffc4225169dc9ca33d55915;hb=a48c5f0f412bbb8c1d6601dd5e11e5c3746f11d5;hp=0ef1ca981f4f86377d3aac9141b5d773e18a8def;hpb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;p=helm.git

diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml
index 0ef1ca981..9e1dcde0d 100644
--- a/helm/ocaml/mathql_test/mqgtop.ml
+++ b/helm/ocaml/mathql_test/mqgtop.ml
@@ -157,8 +157,8 @@ let locate name =
 
 let mpattern n m l =
    let queries = ref [] in
-   let univ = Some [G.builtin G.MainHypothesis; G.builtin G.InHypothesis;
-                    G.builtin G.MainConclusion; G.builtin G.InConclusion] in
+   let univ = Some [G.builtin "MH"; G.builtin "IH";
+                    G.builtin "MC"; G.builtin "IC"] in
    let handle = get_handle () in
    let rec pattern level = function
       | []           -> ()
@@ -194,11 +194,10 @@ let mpattern n m l =
 let mbackward n m l =
    let queries = ref [] in
    let torigth_restriction (u, b) =
-      let p = if b then G.builtin G.MainConclusion 
-                   else G.builtin G.InConclusion in
+      let p = if b then G.builtin "MC" else G.builtin "IC" in
       (u, p, None)
    in
-   let univ = Some [G.builtin G.MainConclusion; G.builtin G.InConclusion] in
+   let univ = Some [G.builtin "MC"; G.builtin "IC"] in
    let handle = get_handle () in
    let rec backward level = function
       | []           -> ()