]> matita.cs.unibo.it Git - helm.git/commit
check_is_really_smaller simplified to consider that it is called only on terms
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 15 Apr 2008 20:52:43 +0000 (20:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 15 Apr 2008 20:52:43 +0000 (20:52 +0000)
commit8c09c56656b3ce07d3f66e7d6ca848cb918b84bd
treeef9c2f3e3f638bb95d96f014880c10e52c558c3b
parent9f66cc89caf70d20a0e4c0d55796da6082d60976
check_is_really_smaller simplified to consider that it is called only on terms
(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.
helm/software/components/cic_proof_checking/cicTypeChecker.ml