minor changes to make the library compile after wilmers new exists.

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

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 115ddfb15b27fa5ad3868e9bef6d54ff5149bbb7..2e94d9c8d0d65b0642d8f0a6b127ae6fb20e8a03 100644 (file)
--- 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