X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnifHint.mli;h=7b8536ba77e98a937d161c4c6c88630fde4bded7;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=21820ace4f98ca6a70f81bdf9227de790aa25633;hpb=c7a74f0ef29118fc97c1a6283f4249a0ed4b0ba1;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 21820ace4..7b8536ba7 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -13,15 +13,21 @@ type db -val index_hint: - db -> NCic.context -> NCic.term -> NCic.term -> int -> db +class status : + object ('self) + method uhint_db: db + method set_uhint_db: db -> 'self + method set_unifhint_status: < uhint_db : db; .. > -> 'self + end -val add_user_provided_hint : db -> NCic.term -> int -> db +val index_hint: + #status as 'status -> NCic.context -> NCic.term -> NCic.term -> int -> 'status -val empty_db : db +val add_user_provided_hint : + #status as 'status -> NCic.term -> int -> 'status val look_for_hint: - db -> + #status -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> (NCic.metasenv *