A .cmo file inside a .cma is linked iff it is referenced at least once.

This was not the case for cicCooking, that simply worked using side-effects
(i.e. registering one function of him to cicEnvironment).

So, I have created a new init function to initialize the wall proof-checker.

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index 86bf3166047ef03b0654aca9bd5360c8a0a9ec09..12c8cd15c4e5cdf2aba454423092e8a2038dfca4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -214,4 +214,6 @@ let cook_obj obj uri =
     cook_all_levels obj (List.rev params)
 ;;
 
-CicEnvironment.set_cooking_function cook_obj;;
+let init () =
+   CicEnvironment.set_cooking_function cook_obj
+;;

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.mli b/helm/ocaml/cic_proof_checking/cicCooking.mli
index 203bf6c33bb4a54935bc548df683c1eb2ea8d7b8..960fb6fae11766b54ba94792635963bcdebcaf89 100644 (file)
--- 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