]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da5cf21) | patch
Pairs are now records.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 12 Dec 2011 16:52:47 +0000 (16:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 12 Dec 2011 16:52:47 +0000 (16:52 +0000)
commitbf5696fc20ffbe552ecb1cd8af0d6fc78d1de9e8
tree05d85ef8e163f6a767a8269d0d360b83977428f5tree | snapshot
parentda5cf21f33e7303bf9b1fc60470de1f6101714ddcommit | diff
Pairs are now records.

Pros: projections from concrete records are now automatically reduced away.
Cons: the name of the constructor is no longer pair, but mk_Prod.
matita/matita/lib/basics/types.ma diff | blob | history
matita/matita/lib/re/moves.ma diff | blob | history
matita/matita/lib/re/re.ma diff | blob | history
matita/matita/lib/re/reb.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.