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