]> matita.cs.unibo.it Git - helm.git/commit
put_inductive_definition implemented and exposed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 14:50:31 +0000 (14:50 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 14:50:31 +0000 (14:50 +0000)
commit1bd58ea9bfc5b8fc2534ba6698fb6afd9c4c9404
treec5c6161a2f9a2bd381bbab4270d8a7ea9368a118
parenta0e5816092e0d90329602192c89d6f320d5fb882
put_inductive_definition implemented and exposed.
It is a very UNSAFE solution to the problem of computing inner-types of
non-debrujined mutual inductive types (whose constructors referes to
the not-yet-defined inductive type block): you can use this function to
add the block to the environment; then you compute the inner-types; and
finally you save the object and register it to the getter.
helm/ocaml/cic_proof_checking/cicEnvironment.ml
helm/ocaml/cic_proof_checking/cicEnvironment.mli