]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3bd3d3a) | patch
Fixed a bug in the discrimination principle: the refiner was not able to
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 12 Jan 2010 12:23:37 +0000 (12:23 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 12 Jan 2010 12:23:37 +0000 (12:23 +0000)
commit829b998d08ec1bfcd68e82b42c369e1e35eb5bed
tree9abbe50cbd17aaaeca7a921fdf501b451fe15d34tree | snapshot
parent3bd3d3ab850c919b64e1eafc65a8cbd5499fd3b8commit | diff
Fixed a bug in the discrimination principle: the refiner was not able to
synthesize the return type of the inner match correctly.
helm/software/components/ng_tactics/nDestructTac.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.