#
# ChangeLog for src/RTLabs
#
# Generated by Trac 1.2
# Dec 10, 2019, 11:54:34 AM

Wed, 07 Dec 2011 15:24:35 GMT campbell [1594]
	* src/RTLabs/Traces.ma (modified)

	Rework handling of termination information in RTLabs structured ...


Mon, 05 Dec 2011 12:11:50 GMT campbell [1586]
	* src/RTLabs/Traces.ma (modified)

	RTLabs structured traces: cost labels after jumps.


Fri, 02 Dec 2011 12:02:08 GMT campbell [1583]
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	More on RTLabs structured traces.
	Fixed mistake in structure trace ...


Mon, 28 Nov 2011 16:57:47 GMT campbell [1574]
	* src/RTLabs/Traces.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	A little more progress on traces on RTLabs.


Fri, 25 Nov 2011 16:30:20 GMT campbell [1565]
	* src/RTLabs/Traces.ma (modified)

	Note that RTLabs ought to classify branches as "jumps" (in the ...


Fri, 25 Nov 2011 12:49:27 GMT campbell [1563]
	* src/RTLabs/Traces.ma (modified)

	A little progress on constructing RTLabs structured traces.


Thu, 24 Nov 2011 17:49:51 GMT campbell [1559]
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)

	Add a notion of flat traces with evidence for RTLabs.


Thu, 24 Nov 2011 11:12:32 GMT campbell [1552]
	* src/RTLabs/Traces.ma (modified)

	Update RTLabs structured trace definition.


Wed, 23 Nov 2011 11:27:55 GMT campbell [1537]
	* src/RTLabs/Traces.ma (added)

	A preliminary definition of the abstract status record for RTLabs.


Wed, 23 Nov 2011 11:07:01 GMT campbell [1535]
	* src/RTLabs/semantics.ma (modified)
	* src/common/Identifiers.ma (modified)

	Make RTLabs semantics use knowledge that the next instruction always ...


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


Fri, 14 Oct 2011 08:56:45 GMT campbell [1369]
	* 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/RTLabs/syntax.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Values.ma (modified)

	Put type information into front-end unary ops.
	Slight change to ...


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 10:26:39 GMT campbell [1316]
	* src (modified)
	* src/ASM (modified)
	* src/ASM/BitVectorTrie.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/syntax.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/deppair.ma (copied)
	* src/utilities/extralib.ma (modified)
	* src/utilities/lists.ma (modified)
	* src/utilities/option.ma (modified)
	* src/utilities/pair.ma (copied)

	Merge in id-lookup-branch to trunk.


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


Thu, 06 Oct 2011 12:08:53 GMT mulligan [1307]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	adding translate_cst


Thu, 06 Oct 2011 09:19:25 GMT mulligan [1306]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	small changes to rtlabs.  what axioms remain look hard to close. ...


Wed, 05 Oct 2011 15:53:54 GMT mulligan [1296]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/adt/table_adt.ma (modified)

	changes


Wed, 05 Oct 2011 12:47:19 GMT mulligan [1293]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	finished rtl abs to rtl transformation subject to closing some axioms ...


Wed, 05 Oct 2011 09:15:00 GMT mulligan [1292]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more added to rtlabs translation


Tue, 04 Oct 2011 00:00:54 GMT sacerdot [1290]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	One more function ported to new Joint.


Mon, 03 Oct 2011 15:33:11 GMT mulligan [1288]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more added to rtlabs to rtl pass


Mon, 03 Oct 2011 14:55:17 GMT mulligan [1287]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	about 3/4 of the way through rtlabs to rtl now


Mon, 03 Oct 2011 14:07:22 GMT mulligan [1286]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more changes to the rtl abs to rtl pass


Mon, 03 Oct 2011 13:08:21 GMT mulligan [1285]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/adt/table_adt.ma (modified)

	more implementation on maps, final push to get rtl abs to rtl working


Fri, 30 Sep 2011 01:12:40 GMT sacerdot [1283]
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/joint/TranslateUtils.ma (modified)

	Bad programming practice removed: change_label is no longer required ...


Wed, 28 Sep 2011 21:50:32 GMT sacerdot [1282]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/Interference.ma (modified)
	* src/ERTL/build.ma (deleted)
	* src/ERTL/liveness.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/TranslateUtils.ma (modified)

	Cosmetic change: names of joint statements/instructions shortened and ...


Wed, 28 Sep 2011 21:08:37 GMT sacerdot [1281]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/joint/semantics.ma (modified)

	Porting of all transformation to the joint syntax practically ...


Wed, 28 Sep 2011 00:43:37 GMT sacerdot [1280]
	* src/ERTL/ERTL.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/TranslateUtils.ma (added)

	Some progress in the porting of RTLAbstoRTL to the joint syntax:

	1) ...


Wed, 21 Sep 2011 15:21:39 GMT sacerdot [1239]
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	RTLAbstoRTL ported to new datatypes.

	Note: RTL syntax/semantics is ...


Wed, 21 Sep 2011 14:25:36 GMT campbell [1238]
	* src/Clight/test/search.c.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/RTLabs/semantics.ma (modified)

	Update Cminor and RTLabs to fit SmallstepExec changes.


Fri, 16 Sep 2011 17:16:44 GMT campbell [1226]
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/test/sum.c.ma (modified)
	* src/Clight/test/sum.test.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/search.Cminor.ma (modified)
	* src/Cminor/test/search.test.ma (added)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/test/search.RTLabs.ma (modified)
	* src/RTLabs/test/search.test.ma (added)

	Adjust pretty printers for change in program records, try a test of
	each.


Fri, 16 Sep 2011 16:39:05 GMT sacerdot [1224]
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/search.c.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IntValue.ma (deleted)

	Type of programs in common/AST made more dependent.
	In particular, ...


Wed, 31 Aug 2011 10:15:39 GMT campbell [1157]
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/test/duff.c.ma (modified)
	* src/Clight/test/factorial.c.ma (modified)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/search.Cminor.ma (modified)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/test/search.RTLabs.ma (modified)

	Update pretty printers and examples.


Tue, 30 Aug 2011 14:22:54 GMT mulligan [1149]
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	changes to get everything type checking again after changing names of ...


Tue, 30 Aug 2011 14:09:20 GMT campbell [1147]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Remove some obsolete commented out code, update a couple of comments.


Tue, 30 Aug 2011 10:47:18 GMT campbell [1139]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/insertsort.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/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Shift init_data out of generic program record so that it only appears ...


Tue, 30 Aug 2011 10:08:25 GMT mulligan [1138]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTLI.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other


Mon, 29 Aug 2011 12:34:23 GMT sacerdot [1123]
	* src/RTLabs/semantics.ma (modified)

	Added comment about missing alignment of data in memory.


Fri, 26 Aug 2011 16:47:25 GMT sacerdot [1116]
	* src/RTLabs/syntax.ma (modified)

	Some comments.


Tue, 19 Jul 2011 10:23:32 GMT mulligan [1077]
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Identifiers.ma (modified)

	ack, dependent types are scary


Fri, 15 Jul 2011 15:38:37 GMT mulligan [1073]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more changes from today


Fri, 15 Jul 2011 14:56:04 GMT campbell [1072]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/Identifiers.ma (modified)

	Use not equals form of showing entry/exit labels.


Fri, 15 Jul 2011 12:40:40 GMT mulligan [1071]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	changes the specific form that the added proofs take to use None, not ...


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.


Thu, 14 Jul 2011 12:27:41 GMT mulligan [1068]
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Identifiers.ma (modified)

	rtlabs translation complete subject to axioms


Wed, 13 Jul 2011 15:37:42 GMT mulligan [1067]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more smaller changes


Wed, 13 Jul 2011 15:12:10 GMT mulligan [1066]
	* src/ASM/I8051.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/Compare.ma (modified)

	changes from today


Tue, 12 Jul 2011 15:52:07 GMT mulligan [1064]
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	changes from today, nearly complete rtlabs translation pass


Mon, 11 Jul 2011 15:52:11 GMT mulligan [1063]
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	changes from today


Mon, 11 Jul 2011 12:09:03 GMT mulligan [1062]
	* src/ASM/FoldStuff.ma (modified)
	* src/ASM/JMCoercions.ma (added)
	* src/ASM/Util.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	separated jmeq and coercions from foldstuff.ma in order to fix the ...


Fri, 08 Jul 2011 15:49:22 GMT mulligan [1061]
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more work, bug found, ridiculous map3 function with dep. types added


Fri, 08 Jul 2011 10:17:14 GMT mulligan [1060]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	work from this morning and yesterday


Wed, 06 Jul 2011 16:09:39 GMT mulligan [1059]
	* src/ASM/Util.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/IntValue.ma (modified)

	work from today, bit of a mess at the moment


Tue, 05 Jul 2011 15:53:11 GMT mulligan [1057]
	* src/ASM/Util.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/IntValue.ma (added)

	changes from today


Tue, 05 Jul 2011 14:25:41 GMT campbell [1056]
	* src/Clight/label.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/Identifiers.ma (modified)

	Switch to delayed identifier error scheme.


Mon, 04 Jul 2011 16:20:23 GMT mulligan [1053]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Identifiers.ma (modified)

	changes


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, 04 Jul 2011 11:49:31 GMT mulligan [1051]
	* src/RTLabs/syntax.ma (modified)

	removed superfluous addressing mode code from RTLabs/syntax.ma


Mon, 04 Jul 2011 08:43:37 GMT mulligan [1050]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/HMap.ma (modified)

	adding dependent types to map datastructure to remove all option ...


Fri, 01 Jul 2011 15:45:46 GMT mulligan [1049]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Order.ma (added)
	* src/common/Registers.ma (modified)
	* src/utilities/HMap.ma (modified)

	more stuff added


Wed, 29 Jun 2011 15:38:27 GMT mulligan [1047]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	more work from today


Wed, 29 Jun 2011 10:15:09 GMT mulligan [1046]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)

	syntax of rtlabs was wrong: cast not const.  more added to rtlabs --> ...


Wed, 29 Jun 2011 08:47:39 GMT mulligan [1045]
	* src/ASM/AssemblyProof.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)

	resolved conflict in rtlabs


Wed, 15 Jun 2011 14:15:57 GMT campbell [967]
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/test/search.RTLabs.ma (modified)
	* src/RTLabs/test/sum.RTLabs.ma (modified)

	Update RTLabs pretty printer and examples.


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


Wed, 08 Jun 2011 11:14:55 GMT campbell [898]
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/null-op.Cminor.ma (added)
	* src/Cminor/test/null-op.ma (deleted)
	* src/Cminor/test/search.Cminor.ma (added)
	* src/Cminor/test/search.ma (deleted)
	* src/Cminor/test/sum.ma (deleted)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/test/search.RTLabs.ma (added)
	* src/RTLabs/test/sum.RTLabs.ma (added)

	Update pretty printers and examples.


Mon, 06 Jun 2011 14:28:07 GMT campbell [888]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Use simplified conditionals in RTLabs, following the prototype.


Mon, 06 Jun 2011 13:55:23 GMT campbell [887]
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Start bringing RTLabs into line with the prototype compiler:
	 - a ...


Fri, 03 Jun 2011 15:35:32 GMT campbell [882]
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/AST.ma (modified)
	* src/utilities/extralib.ma (modified)

	Fix up fragile proofs for current version of matita.


Fri, 03 Jun 2011 15:35:30 GMT campbell [879]
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/factorial.ma (modified)
	* src/Cminor/test/null-op.ma (modified)
	* src/Cminor/test/search.ma (modified)
	* src/Cminor/test/sum-bad.ma (modified)
	* src/Cminor/test/sum.ma (modified)
	* src/Cminor/test/switcher.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/test/search.ma (modified)
	* src/RTLabs/test/sum.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/IO.ma (modified)

	Refine "AST" types to include size/signedness information.


Fri, 03 Jun 2011 15:35:27 GMT campbell [878]
	* src/Cminor/syntax.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Removal of manually inserted record projections.


Thu, 19 May 2011 13:06:42 GMT campbell [816]
	* src/CHANGES (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/toCminor.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/test/factorial.ma (modified)
	* src/Cminor/test/search.ma (modified)
	* src/Cminor/test/switcher.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/RTLabs/test/search.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/lists.ma (modified)

	Clight to Cminor compilation, modulo switch statements, temporary ...


Fri, 13 May 2011 15:35:04 GMT mulligan [799]
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more changes.


Fri, 13 May 2011 11:10:23 GMT campbell [797]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/sum-bad.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/debug.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PreIdentifiers.ma (added)
	* src/common/SmallstepExec.ma (modified)
	* src/common/Values.ma (modified)

	Add error messages wherever the error monad is used.
	Sticks to ...


Fri, 13 May 2011 10:29:06 GMT mulligan [795]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	Changes from this morning.


Thu, 12 May 2011 15:33:22 GMT mulligan [793]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	Work from today on rtlabs -> rtl pass.


Tue, 10 May 2011 15:36:11 GMT mulligan [789]
	* src/RTLabs/RTLAbstoRTL.ma (added)
	* src/common/AssocList.ma (added)

	More work on rtlabs -> rtl pass.


Wed, 27 Apr 2011 09:47:38 GMT campbell [775]
	* src/RTLabs/debug.ma (added)

	A few useful definitions for when RTLabs programs fail.


Tue, 26 Apr 2011 14:51:44 GMT campbell [774]
	* src/CHANGES (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Separate out the different forms of addition and subtraction in the ...


Thu, 21 Apr 2011 17:24:04 GMT campbell [766]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/utilities/lists.ma (added)

	Most of the Cminor to RTLabs stage.

	Is buggy, generates inefficient ...


Wed, 20 Apr 2011 15:39:00 GMT campbell [765]
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/RTLabs/test/search.ma (modified)
	* src/RTLabs/test/sum.ma (added)

	Remove superfluous register in RTLabs return statements.

	Also fix ...


Wed, 20 Apr 2011 15:38:58 GMT campbell [764]
	* src/ASM/Util.ma (modified)
	* src/Cminor/toRTLabs.ma (added)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Errors.ma (modified)

	Start Cminor to RTLabs phase.

	Includes some syntax for matching ...


Tue, 19 Apr 2011 15:48:45 GMT campbell [762]
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (moved)
	* src/RTLabs/syntax.ma (moved)

	Make naming of RTLabs files more uniform


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, 13 Apr 2011 16:52:10 GMT campbell [751]
	* src/Cminor (added)
	* src/Cminor/cminorMatitaPrinter.ml (added)
	* src/Cminor/semantics.ma (added)
	* src/Cminor/syntax.ma (added)
	* src/Cminor/test (added)
	* src/Cminor/test/factorial.ma (added)
	* src/Cminor/test/search.ma (added)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/common/Values.ma (modified)

	Initial version of the Cminor syntax and semantics.


Tue, 12 Apr 2011 10:32:33 GMT campbell [750]
	* src/CHANGES (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/RTLabs/RTLabs-syntax.ma (modified)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/test/search.ma (modified)

	Track some of the changes to the prototype in RTLabs.

	Just one ...


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