From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 13 Dec 2002 12:39:01 +0000 (+0000)
Subject: MathQL textual lexer patched
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca1b7e40c0cce4caba1db40dd18a4ec671c0e59e;p=helm.git

MathQL textual lexer patched
topLevel patched for compilation: -B and -MB don't work
---

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index d021cce85..338db29a7 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -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