mQueryLevels2.mli added in Makefile.

[helm.git] / helm / gTopLevel / topLevel / topLevel.ml

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 745be0767a6b137a7937447e20b2757a5e929316..d021cce856eb3c69c49b76c0db45b465f760a47a 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -108,10 +108,17 @@ let mbackward n m l =
            if Mqint.get_stat () then 
               print_string ("? " ^ CicPp.ppterm term ^ nl);
            let t0 = Sys.time () in
+           
+           
+           
+           
+           
            let list_of_must,can = MQueryLevels.out_restr [] [] term in
            let len = List.length list_of_must in
            let must = if level < len then List.nth list_of_must level else can in
-           let r = Gen.searchPattern [] [] term must can in
+          
+          
+           let r = Gen.searchPattern must can in
            let t1 = Sys.time () -. t0 in
            let info = Gen.get_query_info () in
            let num = List.nth info 0 in