]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ca41435) | patch
removed <_,_> notation second interpretation for dependent pair, since it used
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 24 Jun 2008 18:48:31 +0000 (18:48 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 24 Jun 2008 18:48:31 +0000 (18:48 +0000)
commit59f65aaf6f8d23748e1294ecabffffaa903ae657
tree96578838afb56ac8ab35b66689174da2c21df297tree | snapshot
parentca41435a6021292ccba239aa173651c0be705b45commit | diff
removed <_,_> notation second interpretation for dependent pair, since it used
to have an exponential slowdown on refinement of huge terms....
helm/software/matita/contribs/dama/dama/cprop_connectives.ma diff | blob | history
helm/software/matita/contribs/dama/dama/lebesgue.ma diff | blob | history
helm/software/matita/contribs/dama/dama/models/q_function.ma diff | blob | history
helm/software/matita/contribs/dama/dama/ordered_uniform.ma diff | blob | history
helm/software/matita/contribs/dama/dama/property_exhaustivity.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.