]> matita.cs.unibo.it Git - helm.git/commitdiff
MathQL textual lexer patched
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 13 Dec 2002 12:39:01 +0000 (12:39 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 13 Dec 2002 12:39:01 +0000 (12:39 +0000)
topLevel patched for compilation: -B and -MB don't work

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