- match cmd with
- | GrafiteAst.Coercion _
- | GrafiteAst.Default _
- | GrafiteAst.Drop _
- | GrafiteAst.Print _
- | GrafiteAst.Include _
- | GrafiteAst.Qed _
- | GrafiteAst.Set _ as 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
- lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+ match cmd with
+ | GrafiteAst.Coercion _
+ | GrafiteAst.Default _
+ | GrafiteAst.Drop _
+ | GrafiteAst.Include _
+ | GrafiteAst.Print _
+ | GrafiteAst.Qed _
+ | GrafiteAst.Set _ as 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
+ lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+ | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
+ let lexicon_status_ref = ref lexicon_status in
+ let disambiguate_term =
+ disambiguate_term text prefix_len lexicon_status_ref [] in
+ let disambiguate_term_option metasenv =
+ function
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term metasenv t in
+ metasenv, Some t
+ in
+ let metasenv,a = disambiguate_term metasenv a in
+ let metasenv,aeq = disambiguate_term metasenv aeq in
+ let metasenv,refl = disambiguate_term_option metasenv refl in
+ let metasenv,sym = disambiguate_term_option metasenv sym in
+ let metasenv,trans = disambiguate_term_option metasenv trans in
+ !lexicon_status_ref, metasenv,
+ GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)