X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.mli;h=2df108697cc2fcf6518d2e2f22d362b31519e1ad;hb=6ca487df4f361fd6b0a3b0734396bc6a62b520c3;hp=7414770807cd2dde41355286ce4b8150cc90ba2e;hpb=62f476a05884d451bfb90d845ea2b1c0a1c77f96;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index 741477080..2df108697 100644
--- 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 ->