unification hints almost ready

[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 2e94d9c8d0d65b0642d8f0a6b127ae6fb20e8a03..076ac2f628cc175eaf022a3b43820fdd0fbed877 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -14,11 +14,11 @@
 type db
 
 val index_hint: 
-  db -> NCic.context -> NCic.term -> NCic.term -> db
+  db -> NCic.context -> NCic.term -> NCic.term -> int -> db
 
   (* gets the old imperative coercion DB *)
 val db : unit -> db
-val add_user_provided_hint : Cic.term -> unit 
+val add_user_provided_hint : Cic.term -> int -> unit 
 
 val empty_db : db