From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 15 Jul 2005 23:39:10 +0000 (+0000)
Subject: fixed a specific case in development handling
X-Git-Tag: pre_notation~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9037b899d25db7e09e90e9b4689f073f0dc4c729;p=helm.git

fixed a specific case in development handling
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4f6627fcd..4a6115813 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -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