Huge commit with several changes:

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 5ded5b886370c7c9230e9bfd6323e7be8522db3c..6e72042e83c6a34901de94fe5607e6f41ecc9088 100644 (file)
--- 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) ->