]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0189703) | patch
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
treea86af59d647aa9f7ad5b8b5678d90735401ca983tree | snapshot
parent0189703896b7a3392797132720e5c72fc83eb38ecommit | diff
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 diff | blob | history
helm/ocaml/cic_proof_checking/cicTypeChecker.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.