]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed a specific case in development handling
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 15 Jul 2005 23:39:10 +0000 (23:39 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 15 Jul 2005 23:39:10 +0000 (23:39 +0000)
helm/matita/matitaScript.ml

index 4f6627fcd7d5035dd5b4ab399ebf8e7f3f05557d..4a6115813e708ecbaf57c6394a155a5c62fd142d 100644 (file)
@@ -78,7 +78,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   let module TAPp = TacticAstPp in
   let include_ = 
     match guistuff.filenamedata with
-    | _,None -> []
+    | None,None -> []
     | None,Some devel -> [MatitamakeLib.root_for_development devel ]
     | Some f,_ -> 
         match MatitamakeLib.development_for_dir (Filename.dirname f) with