]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b5036f4) | patch
Bug fixed: checking inductive type declarations with left parameters (e.g.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Feb 2004 12:07:08 +0000 (12:07 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Feb 2004 12:07:08 +0000 (12:07 +0000)
commit422943b59c046b00e4726c18163eeec62f4a82fb
tree7d8594f01d9aecae96167585a056cd92bb1b0816tree | snapshot
parentb5036f4cab9d3942af90e63a877414522bc738cecommit | diff
Bug fixed: checking inductive type declarations with left parameters (e.g.
le) lead to mistakes due to debrujin/undebrujin: terms to be debrujined must
be closed and then left parameters can not be removed _before_ calling
debrujin_constructor.
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.