]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1641d37) | patch
Ambiguous parsing improved: refining is now used to prune-out not-well-typed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Dec 2002 21:36:52 +0000 (21:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Dec 2002 21:36:52 +0000 (21:36 +0000)
commite6e4f76ce06af1f10366bcc094a4be0df3ae8caa
treeb81b637897481f616f969e1a547ee4bb798d28b1tree | snapshot
parent1641d372cb167eb85984d5491f076727bea3d6eacommit | diff
Ambiguous parsing improved: refining is now used to prune-out not-well-typed
choices as soon as the term can not be refined. Unfortunately the whole
disambiguation is parsing-bound and not type-checking/refining bound.
helm/gTopLevel/gTopLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.