From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 11:55:48 +0000 (+0000)
Subject: include must not add aliases in the script!
X-Git-Tag: PRE_GETTER_STORAGE~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d35ebb97d65531bc4e5b51157f44b014e1dcf62;p=helm.git

include must not add aliases in the script!
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 83aa60362..9ca48d9ca 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -83,8 +83,8 @@ let eval_with_engine status user_goal parsed_text st =
   let new_status = MatitaEngine.eval_ast status st in
   let new_aliases =
     match ex with
-      | TA.Command (_, TA.Alias _) ->
-          DisambiguateTypes.Environment.empty
+      | TA.Command (_, TA.Alias _)
+      | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
       | _ -> MatitaSync.alias_diff ~from:status new_status
   in
   (* we remove the defined object since we consider them "automathic aliases" *)