]> matita.cs.unibo.it Git - helm.git/commit
typecheck_mutual_inductive_defs exposed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 14:34:05 +0000 (14:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 14:34:05 +0000 (14:34 +0000)
commita0e5816092e0d90329602192c89d6f320d5fb882
treea86af59d647aa9f7ad5b8b5678d90735401ca983
parent0189703896b7a3392797132720e5c72fc83eb38e
typecheck_mutual_inductive_defs exposed.
It is used to type-check and inductive definition which has no URI associated
to it (i.e. it is not managed by the getter; e.g. when it is not saved yet
since we do not know if it is well-typed).
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.mli