]> matita.cs.unibo.it Git - helm.git/commit
The disambiguation now returns a list of interpretations.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Mar 2004 13:20:11 +0000 (13:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Mar 2004 13:20:11 +0000 (13:20 +0000)
commit29442b4d21cf07992ad4e5c981085dada1f90fe4
tree3f65fa19631d3651dc71fdd425fe79c7a63b88f1
parentdccf88890f1f9f8c8139f67aa7a26f8339b13502
The disambiguation now returns a list of interpretations.

Note: the regtest is broken by this commit.
helm/gTopLevel/batchParser.ml
helm/gTopLevel/batchParser.mli
helm/gTopLevel/disambiguatingParser.mli
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/oldDisambiguate.ml
helm/gTopLevel/oldDisambiguate.mli
helm/gTopLevel/regtest.ml
helm/gTopLevel/termEditor.ml
helm/gTopLevel/testlibrary.ml
helm/gTopLevel/texTermEditor.ml