]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39b862c) | patch
The definition of small inductive types has been relaxed: a constructor
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 5 Dec 2001 14:58:46 +0000 (14:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 5 Dec 2001 14:58:46 +0000 (14:58 +0000)
commit08c377253d9e6131090e273f63d896ec40127cc5
tree4d160cf239247a7dc2cbadc88fea7de632953e3etree | snapshot
parent39b862c075fad2536c35ed3515a0b1ffd478681acommit | diff
The definition of small inductive types has been relaxed: a constructor
is now considered small when its type without the parameters was small
with the previous definition. This is consistent with Coq's behaviour.
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.