BIG FAT WARNING: DEVELOPMENTS DIE HERE

[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 53142e252bfe90a135405bfe32dd00c008d7b91d..ca3bc0b90592bb623e5d1199903afadc6c39573e 100644 (file)
--- 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