urimanager removed

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

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index 5f2ac335d3cba50be6fcbf3cf74da070048978c7..c465fe1d8cd48f16e2b00968a0c6df1f14b2bf02 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -27,12 +27,6 @@
 
 exception BaseUriNotSetYet
 
-(*
-type tactic = 
- (NotationPt.term, NotationPt.term, 
-  NotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic *)
-   
 let singleton msg = function
   | [x], _ -> x
   | l, _   ->
@@ -58,7 +52,6 @@ let ncic_mk_choice = function
            | false -> NCic.Implicit `Term)
         ~mk_appl:(function 
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
-        ~term_of_uri:(fun _ -> assert false)
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
@@ -213,7 +206,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
    estatus, cic
 ;;
 
-let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
+let disambiguate_command estatus (text,prefix_len,cmd)=
   match cmd with
    | GrafiteAst.Include _
    | GrafiteAst.Print _