]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 18ee8c1) | patch
This commit avoids cleaning dummy dependent types in the arities of inductive
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 18 May 2008 17:31:41 +0000 (17:31 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 18 May 2008 17:31:41 +0000 (17:31 +0000)
commit267fbbcd1b8c54ce7faafd48cface965d0f6c37b
treeec34caff028d8ecb36ba42281c4041d24e5ce852tree | snapshot
parent18ee8c139d1fd56d34b97e6b417c0f14d9417886commit | diff
This commit avoids cleaning dummy dependent types in the arities of inductive
types. This is an overkilling solution to the problem of avoiding cleaning
dummy dependent types in the left products in the arities of inductive types.
The left products should be _syntactically_ the same as those of the
constructors. Otherwise, error reporting is incorrect.
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.