]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5965234) | patch
Bug fixed: the outtype of a match when omitted was interpreted as an implicit
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 5 Jul 2005 15:08:10 +0000 (15:08 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 5 Jul 2005 15:08:10 +0000 (15:08 +0000)
commitdc690e0dfa17463d516b74d0a7e5aad810ee1b41
tree289da9deefcc52de37b1922be6ab65f0cd71fdb8tree | snapshot
parent5965234ea82419215b121405fc6dfc53abe4b491commit | diff
Bug fixed: the outtype of a match when omitted was interpreted as an implicit
type (instead it is an implicit term). Thus its type was restricted to be a
sort.
helm/ocaml/cic_disambiguation/disambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.