]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 58004b9) | patch
A .cmo file inside a .cma is linked iff it is referenced at least once.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 Nov 2001 20:47:54 +0000 (20:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 Nov 2001 20:47:54 +0000 (20:47 +0000)
commit94984c5ca3ffd78897e43972965b06645200227a
treeefb0a96afa334936c547ed45b143a501c5b5f842tree | snapshot
parent58004b95e09ac46115883c4d29d69cfa58184e56commit | diff
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 diff | blob | history
helm/ocaml/cic_proof_checking/cicCooking.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.