]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9bc757) | patch
Serious bug fixed: arities of coercions in the .moo files were not computed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 30 Dec 2006 20:56:13 +0000 (20:56 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 30 Dec 2006 20:56:13 +0000 (20:56 +0000)
commit81911249f5f2a6ca774f98a19cd1a34bf1dde384
tree522e3c0694cfab74501e84be76189bc1c446856atree | snapshot
parente9bc7577856e02545d3bc84d8f20aa15c5842034commit | diff
Serious bug fixed: arities of coercions in the .moo files were not computed
correctly. Thus including another file a bugged coercion graph was produced,
with randomic effects quite hard to understand. (Examples in dama where
it was not possible to use <= in place of le here and there because of a
coercion with the wrong arity).
components/grafite_engine/grafiteEngine.ml diff | blob | history
components/grafite_engine/grafiteSync.mli diff | blob | history
components/library/librarySync.ml diff | blob | history
components/library/librarySync.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.