#
# ChangeLog for src/ASM/BitVectorTrie.ma
#
# Generated by Trac 1.2
# Mar 9, 2021, 3:08:43 AM

Mon, 18 Jul 2011 10:44:31 GMT boender [1074]
	* src/ASM/BitVectorTrie.ma (modified)

	- added lookup lemma


Fri, 15 Jul 2011 10:56:48 GMT campbell [1070]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/Identifiers.ma (modified)

	Show that entry and exit labels are in the RTLabs graph.


Mon, 04 Jul 2011 13:31:18 GMT mulligan [1052]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)
	* src/utilities/HMap.ma (modified)

	removed offsets after reading cerco mailing list


Mon, 27 Jun 2011 12:17:25 GMT boender [1044]
	* src/ASM/BitVectorTrie.ma (modified)

	- more fold/forall stuff


Thu, 23 Jun 2011 15:40:43 GMT boender [1038]
	* src/ASM/BitVectorTrie.ma (modified)

	- some more BVT improvements


Wed, 22 Jun 2011 14:03:33 GMT boender [1034]
	* src/ASM/BitVectorTrie.ma (modified)

	various & sundry fold/forall lemmas


Mon, 20 Jun 2011 15:51:51 GMT boender [1006]
	* src/ASM/BitVectorTrie.ma (modified)

	- added fold + lemmas on fold


Fri, 17 Jun 2011 11:30:01 GMT sacerdot [990]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/FoldStuff.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.ma (modified)

	Do no longer use the daemon automatically :-)


Thu, 16 Jun 2011 14:50:23 GMT sacerdot [985]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/common/AST.ma (modified)

	1) Major refactoring: proofs moved where they should be.
	2) New ...


Thu, 28 Apr 2011 15:36:33 GMT mulligan [782]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/RegisterSet.ma (modified)

	More work on rtl-ertl pass from today, plus resolved conflict.


Thu, 28 Apr 2011 08:55:47 GMT campbell [779]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/common/Identifiers.ma (modified)

	Add merging of tries and identifier sets (based on Dominic's earlier ...


Tue, 19 Apr 2011 10:22:32 GMT campbell [761]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/sum-bad.ma (added)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/option.ma (added)

	Enforce the use of declared identifiers/registers in Cminor/RTLabs.


Wed, 30 Mar 2011 16:47:35 GMT campbell [726]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Registers.ma (modified)

	Change identifiers to Words in Clight and RTLabs semantics.


Fri, 18 Mar 2011 12:47:53 GMT mulligan [698]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/String.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/utilities/BitVectorTrieSet.ma (modified)
	* src/utilities/StringTools.ma (modified)

	Commit with changes to files to get our files to typecheck.


Fri, 18 Mar 2011 12:28:33 GMT campbell [697]
	* src/ASM (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/BitVectorZ.ma (copied)
	* src/ASM/Char.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/common/Integers.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/binary/Z.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/oldlib (moved)

	Merge Clight branch of vectors and friends.
	Start making stuff build.


Fri, 18 Mar 2011 10:34:13 GMT mulligan [690]
	* src/ASM/ASM.ma (copied)
	* src/ASM/Arithmetic.ma (copied)
	* src/ASM/BitVector.ma (copied)
	* src/ASM/BitVectorTrie.ma (copied)
	* src/ASM/Char.ma (copied)
	* src/ASM/Fetch.ma (copied)
	* src/ASM/Interpret.ma (copied)
	* src/ASM/Status.ma (copied)
	* src/ASM/String.ma (copied)
	* src/ASM/Util.ma (copied)
	* src/ASM/Vector.ma (copied)
	* src/ASM/new-matita-development (deleted)

	Moved new matita files into correct place.


Fri, 18 Mar 2011 10:31:32 GMT mulligan [688]
	* Deliverables/D4.1/Demo-March-2011 (deleted)
	* Deliverables/D4.2-4.3/LIN/LinToAsm.ma (deleted)
	* src (added)
	* src/ASM (moved)
	* src/LIN (moved)
	* src/LIN/LIN.ma (copied)

	Fixed local conflicts.  Restructured svn repository.