From 08affd483123f36da15b38c89d58a0477bc96244 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 18 Nov 2010 10:45:20 +0000 Subject: [PATCH] - dead code removed --- matita/components/disambiguation/disambiguate.ml | 5 ----- 1 file changed, 5 deletions(-) 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 -- 2.39.2