X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicCooking.mli;h=960fb6fae11766b54ba94792635963bcdebcaf89;hb=2f28bfb47f5fad6b3c5a705d9ede95700416dee8;hp=203bf6c33bb4a54935bc548df683c1eb2ea8d7b8;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.mli b/helm/ocaml/cic_proof_checking/cicCooking.mli
index 203bf6c33..960fb6fae 100644
--- a/helm/ocaml/cic_proof_checking/cicCooking.mli
+++ b/helm/ocaml/cic_proof_checking/cicCooking.mli
@@ -28,4 +28,7 @@ exception NotImplemented of int * string
 exception WrongUriToConstant
 exception WrongUriToVariable of string
 exception WrongUriToInductiveDefinition
-val cook_obj : Cic.obj -> UriManager.uri -> (int * Cic.obj) list
+
+(* init register the cooking function defined in this module so that it *)
+(* will be used to retrieve the cooked objects from the environment     *)
+val init : unit -> unit