First attempt to implement unification hints.

[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 0efb49bff54f039f92b3ff1bbef997fe9091777b..9f14c503f3bc30a99cb9ae29457e7ecb345645ff 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -40,7 +40,8 @@ let refine_term
         assert false
     in
     let metasenv, subst, term, _ = 
-      NCicRefiner.typeof 
+      NCicRefiner.typeof
+        (NCicUnifHint.db ())
         ~look_for_coercion:(
           if use_coercions then 
            NCicCoercion.look_for_coercion coercion_db