From 94984c5ca3ffd78897e43972965b06645200227a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Nov 2001 20:47:54 +0000 Subject: [PATCH] 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. --- helm/ocaml/cic_proof_checking/cicCooking.ml | 4 +++- helm/ocaml/cic_proof_checking/cicCooking.mli | 5 ++++- 2 files changed, 7 insertions(+), 2 deletions(-) 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 -- 2.39.2