]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2865afb) | patch
The parser (the lexer indeed) now use the locate query to locate an object
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Sep 2002 17:53:22 +0000 (17:53 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Sep 2002 17:53:22 +0000 (17:53 +0000)
commit5017b0b1d58b9431129055b82a40f73c979bf3ae
treed911df0883cf46c24451d588495d0d94d09ca09atree | snapshot
parent2865afb3a2ebce0376087c1cd41ab7146a6bdde4commit | diff
The parser (the lexer indeed) now use the locate query to locate an object
whose identifier is unknown. In ambigous cases, no choice is given to the
user and the usual exception (identifier not found) is raised. It works
only for constants and for the first inductive type of a mutual inductive
type block.
helm/gTopLevel/gTopLevel.ml diff | blob | history
helm/gTopLevel/mQueryGenerator.ml diff | blob | history
helm/gTopLevel/mQueryGenerator.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.