From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Dec 2008 21:42:51 +0000 (+0000)
Subject: Useless code removed.
X-Git-Tag: make_still_working~4449
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6110532ca4a8e80f0e867500fcae92bf2f44b899;p=helm.git

Useless code removed.
---

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index ae56682ce..e9afcf01b 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -379,8 +379,6 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
-let domain_of_ast_term = domain_of_term;;
-
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli
index 5c74b857b..822f14092 100644
--- a/helm/software/components/disambiguation/disambiguate.mli
+++ b/helm/software/components/disambiguation/disambiguate.mli
@@ -81,8 +81,6 @@ val resolve :
    [`Num_arg of string | `Args of 'term list] -> 'term
 
 val find_in_context: string -> string option list -> int
-val domain_of_ast_term: context:
-  string option list -> CicNotationPt.term -> domain
 val domain_of_term: context:
   string option list -> CicNotationPt.term -> domain
 val domain_of_obj: 
@@ -124,7 +122,7 @@ val disambiguate_thing:
     'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
       ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
   mk_localization_tbl:(int -> 'cichash) ->
-  string * int * 'ast_thing ->
+  'ast_thing disambiguator_input ->
   ((DisambiguateTypes.Environment.key * 'alias) list * 
    'metasenv * 'subst * 'refined_thing * 'ugraph)
   list * bool
diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 7f9ab1b6e..9e9130857 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -431,10 +431,6 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 ~localization_tbl
 ;;
 
-let domain_of_term ~context = 
-  Disambiguate.domain_of_ast_term ~context
-;; 
-
 let disambiguate_term ~context ~metasenv ~subst ?goal
    ~mk_implicit ~description_of_alias ~mk_choice
    ~aliases ~universe ~coercion_db ~lookup_in_library 
@@ -463,7 +459,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
-     ~lookup_in_library ~domain_of_thing:domain_of_term
+     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
      ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None))
      ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
      ~mk_localization_tbl ~hint ~subst