X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=ca3bc0b90592bb623e5d1199903afadc6c39573e;hb=474586cb3917d3961bbf1e8b818b83073dc510f2;hp=53142e252bfe90a135405bfe32dd00c008d7b91d;hpb=1ca749a387695a5a4abc138a06de496a63abac4a;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 53142e252..ca3bc0b90 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -406,7 +406,7 @@ let rec disambiguate_tactic
 	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
 
 
-let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
+let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
   let uri =
    match obj with
     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
@@ -426,7 +426,7 @@ let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic
   
-let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
+let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
    | GrafiteAst.Index(loc,key,uri) ->
        let lexicon_status_ref = ref lexicon_status in 
@@ -451,7 +451,7 @@ let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->
        let lexicon_status,metasenv,obj =
-        disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in
+        disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
        lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
       let lexicon_status_ref = ref lexicon_status in