#
# ChangeLog for src/RTLabs/syntax.ma
#
# Generated by Trac 1.2
# Mar 4, 2021, 6:06:52 AM

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


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.


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

	adding translate_cst


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


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


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

	Some comments.


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.


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

	removed superfluous addressing mode code from RTLabs/syntax.ma


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


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


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