#
# ChangeLog for src/Clight/casts.ma
#
# Generated by Trac 1.2
# Mar 2, 2021, 5:59:45 PM

Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Policy.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/ASM/WellLabeled.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/casts.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Values.ma (modified)

	!! BEWARE: major commit !!

	1) [affects everybody]
	   split for ...


Tue, 13 Dec 2011 00:34:37 GMT sacerdot [1599]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/JMCoercions.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/String.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/casts.ma (modified)
	* src/Clight/test/search.c.ma (modified)
	* src/Clight/test/sum.test.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/AssocList.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/Floats.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/joint/BEGlobalenvs.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/adt/priority_set_adt.ma (modified)
	* src/utilities/adt/set_adt.ma (modified)
	* src/utilities/adt/table_adt.ma (modified)
	* src/utilities/binary/division.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/lists.ma (modified)
	* src/utilities/pair.ma (deleted)

	Start of merging of stuff into the standard library of Matita.


Fri, 18 Nov 2011 23:38:20 GMT sacerdot [1516]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/BitVectorZ.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.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/casts.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/joint/BEValues.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/extranat.ma (modified)
	* src/utilities/lists.ma (modified)

	Ported to syntax of Matita 0.99.1.


Fri, 04 Nov 2011 11:39:56 GMT campbell [1489]
	* src/Clight/casts.ma (modified)

	Fix up a couple of lemmas affected by the change to add_with_carries.


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, 23 May 2011 15:39:13 GMT campbell [824]
	* src/Clight/casts.ma (added)

	Some work on showing that casts around integer operations can be
	removed.