- oCic2NCic and nCic2OCic moved to ng_library

[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 1e88c3714129f0b06d22c4bf80597ded7ff4bb87..d50eec79600b12358ecd7bc5af9d84f4ae7f4d47 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -22,6 +22,9 @@ module NRef = NReference
 let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
 
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
   | _ -> assert false
@@ -325,7 +328,7 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
+         NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref