]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteDisambiguator.ml
exported disambiguate_thing
[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguator.ml
index 8827e709b42328072edcb01591e9422ef73ba9e1..ddd655bc40a95b5e00ff93748a526e53f3fa1030 100644 (file)
@@ -222,3 +222,5 @@ let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
   let f = Disambiguator.disambiguate_obj ~dbd ~uri in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff obj
+
+let disambiguate_thing = assert false