First attempt to implement unification hints.

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.mli

diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index 7414770807cd2dde41355286ce4b8150cc90ba2e..2df108697cc2fcf6518d2e2f22d362b31519e1ad 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.mli
+++ b/helm/software/components/ng_refiner/nCicRefiner.mli
@@ -16,6 +16,7 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val typeof :
+ NCicUnifHint.db ->
  ?localise:(NCic.term -> Stdpp.location) ->
  look_for_coercion:(
     NCic.metasenv -> NCic.substitution -> NCic.context ->