]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1bd58ea) | patch
First working version of the possibility to introduce new inductive type
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 16:05:50 +0000 (16:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 16:05:50 +0000 (16:05 +0000)
commit0612f5cdb29570e4cf61ef7f40aba91c07f48f62
tree633ea18f3425465fa0b8b13da9a3c8b320e3a3bbtree | snapshot
parent1bd58ea9bfc5b8fc2534ba6698fb6afd9c4c9404commit | diff
First working version of the possibility to introduce new inductive type
definitions. Many checks have not been implemented yet and the interface
allows you to progress to further stages even if the input is incorrect.
Nevertheless, if the input is correct it will be accepted by the kernel,
saved to disk and notified to the getter.

This is the dawn of a new set implementation era.
helm/gTopLevel/gTopLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.