X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=6aee803f42578cf16cb04a5187856470c2f3c48a;hb=68b13bbcf487f7575d5f04f6b2c23aa9ef02409b;hp=b53d6ea3fb6db595178073874e3adc79b89a2416;hpb=63b86fce8a75490b957e7301517b9006f58321b6;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b53d6ea3f..6aee803f4 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -175,6 +175,24 @@ let nlookup_in_library
   | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item 
 ;;
 
+let fix_instance item l =
+ match item with
+    DisambiguateTypes.Symbol (_,n) ->
+     List.map
+      (function
+          LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d)
+        | _ -> assert false
+      ) l
+  | DisambiguateTypes.Num n ->
+     List.map
+      (function
+          LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d)
+        | _ -> assert false
+      ) l
+  | DisambiguateTypes.Id _ -> l
+;;
+
+
   (** @param term not meaningful when context is given *)
 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 term =
@@ -186,7 +204,7 @@ term =
         ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library
         ~mk_choice:cic_mk_choice
-        ~mk_implicit
+        ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~context ~metasenv ~subst:[] (text,prefix_len,term))
   in
@@ -206,7 +224,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
         ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library:nlookup_in_library
         ~mk_choice:ncic_mk_choice
-        ~mk_implicit
+        ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~context ~metasenv ~subst thing)
   in
@@ -228,7 +246,7 @@ let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
         (CicDisambiguate.disambiguate_term 
           ~lookup_in_library
           ~mk_choice:cic_mk_choice
-          ~mk_implicit
+          ~mk_implicit ~fix_instance
           ~description_of_alias:LexiconAst.description_of_alias
           ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases
           ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
@@ -734,7 +752,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
       (CicDisambiguate.disambiguate_obj 
         ~lookup_in_library 
         ~mk_choice:cic_mk_choice
-        ~mk_implicit
+        ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~aliases:estatus#lstatus.LexiconEngine.aliases
         ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) 
@@ -781,7 +799,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~lookup_in_library:nlookup_in_library
       ~description_of_alias:LexiconAst.description_of_alias
       ~mk_choice:ncic_mk_choice
-      ~mk_implicit
+      ~mk_implicit ~fix_instance
       ~uri:(OCic2NCic.nuri_of_ouri uri)
       ~rdb:estatus
       ~aliases:estatus#lstatus.LexiconEngine.aliases