1. grafiteDisambiguator => multiPassDisambiguator

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 24fdadd5e5e1ad0773ae388240618a1a0258012e..ef9da1f2008f04e099175f5b3bb9c0e3cb0fcbe4 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -101,7 +101,7 @@ term =
   let lexicon_status = !lexicon_status_ref in
   let (diff, metasenv, subst, cic, _) =
     singleton "first"
-      (GrafiteDisambiguator.disambiguate_term
+      (MultiPassDisambiguator.disambiguate_term
         ~aliases:lexicon_status.LexiconEngine.aliases
         ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
         ~lookup_in_library
@@ -122,7 +122,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
     let lexicon_status = !lexicon_status_ref in
     let (diff, metasenv, _, cic, ugraph) =
       singleton "second"
-        (GrafiteDisambiguator.disambiguate_term ~lookup_in_library 
+        (MultiPassDisambiguator.disambiguate_term ~lookup_in_library 
           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
           ~context ~metasenv ~subst:[] ?goal
@@ -135,7 +135,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
 let disambiguate_pattern 
   text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path) 
 =
-  let interp path = Disambiguate.interpretate_path [] path in
+  let interp path =CicDisambiguate.interpretate_path [] path in
   let goal_path = HExtlib.map_option interp goal_path in
   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
   let wanted =
@@ -507,12 +507,12 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-(*
+  (*
   (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
        (try
          let [_,_,_,ty],_ =
-          NGrafiteDisambiguator.disambiguate_term
+          NMultiPassDisambiguator.disambiguate_term
            ~context:[] ~metasenv:[] ~subst:[]
            ~aliases:DisambiguateTypes.Environment.empty
            ~universe:(Some DisambiguateTypes.Environment.empty)
@@ -520,16 +520,15 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          in
           prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!!  " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty)
-       with NGrafiteDisambiguator.DisambiguationError _ ->
+       with NMultiPassDisambiguator.DisambiguationError _ ->
         prerr_endline "ERRORE NUOVA DISAMBIGUAZIONE";
         assert false
        | exn -> ())
     | _ -> ()
-  );
-*)
+  ); *)
   let (diff, metasenv, _, cic, _) =
     singleton "third"
-      (GrafiteDisambiguator.disambiguate_obj ~lookup_in_library
+      (MultiPassDisambiguator.disambiguate_obj ~lookup_in_library
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
         (text,prefix_len,obj)) in