From 8d35ebb97d65531bc4e5b51157f44b014e1dcf62 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 11:55:48 +0000 Subject: [PATCH] include must not add aliases in the script! --- helm/matita/matitaScript.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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" *) -- 2.39.2