# # ChangeLog for src/common/Integers.ma # # Generated by Trac 1.2 # Mar 8, 2021, 11:53:48 PM Wed, 15 Jun 2011 14:15:52 GMT campbell [961] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Clight/test/search.ma (modified) * src/Clight/test/sum.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/Events.ma (modified) * src/common/Floats.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) * src/utilities/extranat.ma (modified) Use precise bitvector sizes throughout the front end, rather than ... Mon, 06 Jun 2011 21:07:24 GMT sacerdot [889] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Vector.ma (modified) * src/common/Integers.ma (modified) Minor changes because of the new, weaker (but much faster) delift. Fri, 08 Apr 2011 12:06:46 GMT campbell [747] * src/Clight/AST.ma (deleted) * src/Clight/Csyntax.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Integers.ma (modified) * src/common/Maps.ma (modified) * src/common/Values.ma (modified) * src/utilities/Coqlib.ma (modified) Merge the two AST files together (although some definitions still ... 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 ... 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: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 11:59:56 GMT campbell [695] * src/Clight/depends (deleted) * src/Clight/root (deleted) * src/RTLabs (moved) * src/common/Errors.ma (moved) * src/common/Events.ma (moved) * src/common/Floats.ma (moved) * src/common/FrontEndOps.ma (moved) * src/common/Globalenvs.ma (moved) * src/common/Graphs.ma (moved) * src/common/IOMonad.ma (moved) * src/common/Integers.ma (moved) * src/common/Maps.ma (moved) * src/common/Mem.ma (moved) * src/common/Registers.ma (moved) * src/common/Smallstep.ma (moved) * src/common/SmallstepExec.ma (moved) * src/common/Values.ma (moved) * src/utilities/Coqlib.ma (moved) * src/utilities/binary (moved) * src/utilities/extralib.ma (moved) Rearrange Clight files a bit - will try to make them work again soon... Fri, 18 Mar 2011 11:30:38 GMT campbell [694] * src/Clight (moved) Start moving Clight into common directory.