X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnifHint.mli;h=2e94d9c8d0d65b0642d8f0a6b127ae6fb20e8a03;hb=fdab21f9db0c8536718001e38213c34595170182;hp=115ddfb15b27fa5ad3868e9bef6d54ff5149bbb7;hpb=e6cfe36583259c1e3f6d91e66e50a647726c1716;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 115ddfb15..2e94d9c8d 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -18,6 +18,7 @@ val index_hint:
 
   (* gets the old imperative coercion DB *)
 val db : unit -> db
+val add_user_provided_hint : Cic.term -> unit 
 
 val empty_db : db