]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/topLevel/topLevel.ml
MathQL textual lexer patched
[helm.git] / helm / gTopLevel / topLevel / topLevel.ml
index d021cce856eb3c69c49b76c0db45b465f760a47a..338db29a7107a7ce8a15beb4be48ef2f843c682a 100644 (file)
@@ -112,13 +112,13 @@ let mbackward n m l =
            
            
            
-           
+(* FG: Mettere a posto qui.
            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 must can in
+           let r = [] (* FG e anche qui: 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