X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=6e72042e83c6a34901de94fe5607e6f41ecc9088;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=5ded5b886370c7c9230e9bfd6323e7be8522db3c;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 5ded5b886..6e72042e8 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -312,7 +312,8 @@ let interpretate_term_and_interpretate_term_option
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
     | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
        assert (subst = None);
        (try
@@ -321,12 +322,13 @@ let interpretate_term_and_interpretate_term_option
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
-    | CicNotationPt.Uri (name, subst) ->
+    | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NRef.reference_of_string name)
+         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
+    | CicNotationPt.NRef nref -> NCic.Const nref
     | CicNotationPt.Implicit -> NCic.Implicit `Term
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) ->