Useless code removed.

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index ae56682cef2adbd8fef6ca20c456af16d4e22320..e9afcf01b07c5ec43a9c99ca9099a358050c95c5 100644 (file)
--- 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 5c74b857b49077bd1d68048af460252e5bc023a3..822f14092db739a83cc25e272ada2908f3e64afc 100644 (file)
--- 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 7f9ab1b6e2cdaeec66445d02617a4dbad71b8bcb..9e9130857145c2bb84d74eb718c33625f78d0e3b 100644 (file)
--- 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