# # ChangeLog for src/ASM/Vector.ma # # Generated by Trac 1.2 # Jan 28, 2021, 7:54:02 AM Tue, 12 Apr 2011 10:32:33 GMT campbell [749] * src/ASM/Vector.ma (modified) Make definition more explicit to avoid jmeq. Thu, 07 Apr 2011 16:53:59 GMT campbell [744] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/AST.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/RTLabs/RTLabs-sem.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Integers.ma (modified) * src/common/Mem.ma (modified) * src/common/Values.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/extranat.ma (added) Evict Coq-style integers from common/Integers.ma. Make more ... 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 15:28:26 GMT campbell [700] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorZ.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/AST.ma (modified) * src/Clight/Animation.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/CostLabel.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/common/Events.ma (modified) * src/common/Floats.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Integers.ma (modified) * src/common/Maps.ma (modified) * src/common/Mem.ma (modified) * src/common/Smallstep.ma (modified) * src/common/SmallstepExec.ma (modified) * src/common/Values.ma (modified) Get Clight semantics going again (except for problems CexecEquiv that ... 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.