]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_test/mqgtop.ml
This commit was manufactured by cvs2svn to create tag
[helm.git] / helm / ocaml / mathql_test / mqgtop.ml
index 0ef1ca981f4f86377d3aac9141b5d773e18a8def..9e1dcde0d99dba624ffc4225169dc9ca33d55915 100644 (file)
@@ -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
       | []           -> ()