From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Nov 2010 10:45:20 +0000 (+0000)
Subject: - dead code removed
X-Git-Tag: make_still_working~2694
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=08affd483123f36da15b38c89d58a0477bc96244;p=helm.git

- dead code removed
---

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 8be47f063..c83760782 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -407,11 +407,6 @@ let domain_diff dom1 dom2 =
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
-type alias_spec =
-  | Ident_alias of string * string        (* identifier, uri *)
-  | Symbol_alias of string * int * string (* name, instance no, description *)
-  | Number_alias of int * string          (* instance no, description *)
-
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context