From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 Nov 2001 20:47:54 +0000 (+0000)
Subject: A .cmo file inside a .cma is linked iff it is referenced at least once.
X-Git-Tag: mlminidom_0_2_2~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94984c5ca3ffd78897e43972965b06645200227a;p=helm.git

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 86bf31660..12c8cd15c 100644
--- 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 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