matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 26 Jul 2005 12:24:53 +0000 (12:24 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 26 Jul 2005 12:24:53 +0000 (12:24 +0000)
commit	c12d08acf947823bbfd5909618b042c65ff107de
tree	9601cf4bb5aa4f042370f8a93cf856689b0400c5	tree \| snapshot
parent	35c4cdcf7b072563be3e8c37bf3cc1065a221c50	commit \| diff

**** Experimental: ****

After the disambiguation, if the term is no longer ambiguous, we forget the
environment. In this way we are forced to do more work later (since we have
less aliases), but we have more freedom (since we have less aliases) in the
future disambiguations.

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom

helm/matita/library/Z/orders.ma		diff \| blob \| history
helm/matita/library/Z/times.ma		diff \| blob \| history
helm/matita/library/Z/z.ma		diff \| blob \| history
helm/matita/matita.txt		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguate.ml		diff \| blob \| history