Big commit and major code clean-up:

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index fcbcdea1442cce3be7be508881038f0599ebbce6..f6db501b3f456267cff48818c395f8f722a2e98d 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -63,3 +63,4 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 let disambiguate_term = Disambiguator.disambiguate_term
 
+let disambiguate_obj = Disambiguator.disambiguate_obj