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

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

author	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Wed, 30 Mar 2011 11:52:27 +0000 (11:52 +0000)
committer	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Wed, 30 Mar 2011 11:52:27 +0000 (11:52 +0000)
commit	6d4277977478ef9bcadaffbef3d4bb04ac0250a5
tree	c29d3106489220310d8749a6e596578e54ff624a	tree \| snapshot
parent	98f0fac6d03367be776303e7ba353b75878aaa40	commit \| diff

Keeping track of locations of disambiguated ids and symbols.
Matitac produces disambiguated files, with hyperlinks for ids and § marks
for symbols.
Matita is able to reparse ids with hypelinks.

40 files changed:

matitaB/components/METAS/meta.helm-content_pres.src		diff \| blob \| history
matitaB/components/content/notationEnv.ml		diff \| blob \| history
matitaB/components/content/notationEnv.mli		diff \| blob \| history
matitaB/components/content/notationPp.ml		diff \| blob \| history
matitaB/components/content_pres/Makefile		diff \| blob \| history
matitaB/components/content_pres/cicNotationLexer.ml		diff \| blob \| history
matitaB/components/content_pres/cicNotationParser.ml		diff \| blob \| history
matitaB/components/content_pres/termContentPres.ml		diff \| blob \| history
matitaB/components/content_pres/termContentPres.mli		diff \| blob \| history
matitaB/components/disambiguation/disambiguate.ml		diff \| blob \| history
matitaB/components/disambiguation/disambiguate.mli		diff \| blob \| history
matitaB/components/disambiguation/disambiguateTypes.ml		diff \| blob \| history
matitaB/components/disambiguation/disambiguateTypes.mli		diff \| blob \| history
matitaB/components/disambiguation/multiPassDisambiguator.ml		diff \| blob \| history
matitaB/components/disambiguation/multiPassDisambiguator.mli		diff \| blob \| history
matitaB/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
matitaB/components/grafite_engine/grafiteTypes.ml		diff \| blob \| history
matitaB/components/grafite_engine/grafiteTypes.mli		diff \| blob \| history
matitaB/components/grafite_engine/nCicCoercDeclaration.ml		diff \| blob \| history
matitaB/components/library/librarian.ml		diff \| blob \| history
matitaB/components/ng_disambiguation/grafiteDisambiguate.ml		diff \| blob \| history
matitaB/components/ng_disambiguation/grafiteDisambiguate.mli		diff \| blob \| history
matitaB/components/ng_disambiguation/nCicDisambiguate.ml		diff \| blob \| history
matitaB/components/ng_disambiguation/nCicDisambiguate.mli		diff \| blob \| history
matitaB/components/ng_tactics/nTacStatus.ml		diff \| blob \| history
matitaB/matita/cicMathView.ml		diff \| blob \| history
matitaB/matita/lib/arithmetics/nat.ma		diff \| blob \| history
matitaB/matita/lib/basics/logic.ma		diff \| blob \| history
matitaB/matita/lib/basics/pts.ma		diff \| blob \| history
matitaB/matita/matitaEngine.ml		diff \| blob \| history
matitaB/matita/matitaExcPp.ml		diff \| blob \| history
matitaB/matita/matitaGui.ml		diff \| blob \| history
matitaB/matita/matitaScript.ml		diff \| blob \| history
matitaB/matita/nlibrary/properties/relations.ma		diff \| blob \| history
matitaB/matita/nlibrary/properties/relations1.ma		diff \| blob \| history
matitaB/matita/nlibrary/properties/relations2.ma		diff \| blob \| history
matitaB/matita/nlibrary/sets/setoids.ma		diff \| blob \| history
matitaB/matita/nlibrary/sets/setoids1.ma		diff \| blob \| history
matitaB/matita/nlibrary/sets/setoids2.ma		diff \| blob \| history
matitaB/matita/nlibrary/sets/sets.ma		diff \| blob \| history

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

RSS Atom