From: Andrea Asperti Date: Thu, 23 Nov 2006 14:46:01 +0000 (+0000) Subject: Command index added to disambiguate. X-Git-Tag: 0.4.95@7852~787 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00d934e7be5c77d8f3ee92d6ee39c2e8fc2d880e;hp=00d934e7be5c77d8f3ee92d6ee39c2e8fc2d880e;p=helm.git Command index added to disambiguate. -This line, and those below, will be ignored-- M grafite_parser/grafiteDisambiguate.ml ---