#
# ChangeLog for src/RTLabs/RTLabsToRTL.ma
#
# Generated by Trac 1.2
# Apr 20, 2021, 6:52:39 AM

Thu, 02 Aug 2012 15:04:37 GMT campbell [2290]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	Remove jump tables from RTLabs -> RTL.


Thu, 02 Aug 2012 13:18:11 GMT tranquil [2286]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/ERTLToLTL_paolo.ma (deleted)
	* src/ERTL/ERTL_paolo.ma (deleted)
	* src/ERTL/Interference.ma (modified)
	* src/ERTL/Interference_paolo.ma (deleted)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/liveness_paolo.ma (deleted)
	* src/ERTL/semantics.ma (modified)
	* src/ERTL/semantics_paolo.ma (deleted)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LIN/LIN_paolo.ma (deleted)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LIN/joint_LTL_LIN_paolo.ma (deleted)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics_paolo.ma (deleted)
	* src/LIN/semantics.ma (modified)
	* src/LIN/semantics_paolo.ma (deleted)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/LTL/LTLToLIN_paolo.ma (deleted)
	* src/LTL/LTL_paolo.ma (deleted)
	* src/LTL/semantics.ma (modified)
	* src/LTL/semantics_paolo.ma (deleted)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLTailcall_paolo.ma (deleted)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTL/RTLToERTL_paolo.ma (deleted)
	* src/RTL/RTL_paolo.ma (deleted)
	* src/RTL/semantics.ma (modified)
	* src/RTL/semantics_paolo.ma (deleted)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (deleted)
	* src/common/AST.ma (modified)
	* src/common/BackEndOps.ma (added)
	* src/common/ByteValues.ma (modified)
	* src/common/ByteValues_paolo.ma (deleted)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Registers.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Joint_paolo.ma (deleted)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/TranslateUtils_paolo.ma (deleted)
	* src/joint/blocks.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semanticsUtils_paolo.ma (deleted)
	* src/joint/semantics_paolo.ma (deleted)
	* src/utilities/extranat.ma (modified)

	Big update!

	* merge of all _paolo variants
	* reorganised some ...


Thu, 12 Jul 2012 11:28:28 GMT campbell [2176]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/ClassifyOp.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/test/duff.c.ma (modified)
	* src/Clight/test/insertsort.c.ma (modified)
	* src/Clight/test/memorymodel.ma (modified)
	* src/Clight/test/null-op.c.ma (modified)
	* src/Clight/test/search.c.ma (modified)
	* src/Clight/test/sum.c.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/RTL/semantics.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/FrontEndVal.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/Values.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/semantics.ma (modified)

	Remove memory spaces other than XData and Code; simplify pointers as ...


Thu, 21 Jun 2012 15:21:02 GMT campbell [2103]
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/AST.ma (modified)
	* src/joint/Erasure.ma (modified)

	Make transform_*program take a more general transformation to make ...


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 ...


Thu, 24 May 2012 17:18:35 GMT campbell [1995]
	* src/ERTL/liveness.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/TranslateUtils.ma (modified)

	Overall compiler definition; bits and pieces to
	make everything ...


Tue, 13 Dec 2011 13:49:52 GMT sacerdot [1601]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/semantics.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/common/StructuredTraces.ma (modified)
	* src/joint/BEValues.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	Files ported to new version of the standard library.


Tue, 22 Nov 2011 11:28:04 GMT campbell [1529]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	Update RTLabs to RTL with unary operation types.


Mon, 21 Nov 2011 12:06:01 GMT sacerdot [1521]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/binary/Z.ma (modified)

	Syntax change in Matita: change what where => change where what.


Fri, 18 Nov 2011 12:03:14 GMT campbell [1515]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Erase.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/fresh.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/insertsort.test.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (added)
	* src/common/PreIdentifiers.ma (modified)
	* src/joint/Erasure.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/extranat.ma (modified)

	Add type of maps on positive binary numbers, and use them for ...


Wed, 19 Oct 2011 09:30:24 GMT sacerdot [1408]
	* src/ERTL/semantics.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/LIN/semantics.ma (modified)
	* src/RTL/semantics.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/joint/BEGlobalenvs.ma (added)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/semantics.ma (modified)

	1. Added joint/BEGlobalenvs that is a modification of ...


Tue, 11 Oct 2011 15:48:31 GMT mulligan [1358]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	got rtlabs to rtl compiling, foldi_strong needs examining


Tue, 11 Oct 2011 15:33:11 GMT mulligan [1356]
	* Deliverables/D4.2-4.3/ASM (deleted)
	* Deliverables/D4.2-4.3/reports (added)
	* Deliverables/D4.2-4.3/reports/D4-2.tex (added)
	* Deliverables/D4.2-4.3/reports/D4-3.tex (added)
	* src/RTLabs/RTLabsToRTL.ma (modified)

	deleted redundant directory.  added outlines for both reports, and ...


Tue, 11 Oct 2011 12:38:19 GMT sacerdot [1354]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	One axiom closed.


Tue, 11 Oct 2011 10:45:16 GMT sacerdot [1352]
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/semantics.ma (modified)

	This commit is made necessary by the last Matita change.
	Inclusion ...


Mon, 10 Oct 2011 15:27:34 GMT mulligan [1343]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	fixed some bugs in the translation


Mon, 10 Oct 2011 08:21:35 GMT mulligan [1331]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	some changes, but i now have two contradictory proof obligations.


Fri, 07 Oct 2011 13:45:13 GMT mulligan [1325]
	* src/RTLabs/RTLabsToRTL.ma (modified)

	finished implementing the translate constant function


Fri, 07 Oct 2011 09:12:34 GMT mulligan [1315]
	* src/RTL/RTLToERTL.ma (moved)
	* src/RTLabs/RTLabsToRTL.ma (modified)

	another move for the same reason.  got rtlabs > rtl compiling again ...


Fri, 07 Oct 2011 09:03:38 GMT mulligan [1314]
	* src/RTLabs/RTLabsToRTL.ma (moved)

	name changes so that bash tab completion actually works with some ...


Thu, 06 Oct 2011 15:27:32 GMT mulligan [1308]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	changes to translate_cst