#
# ChangeLog for src/Clight/Csyntax.ma
#
# Generated by Trac 1.2
# Jan 28, 2021, 7:04:42 AM

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


Wed, 30 Mar 2011 14:16:08 GMT campbell [725]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/test/transform1.ma (modified)

	Do some light manual disambiguation to make Clight examples go ...


Tue, 29 Mar 2011 16:21:16 GMT campbell [720]
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-syntax.ma (modified)
	* src/common/CostLabel.ma (moved)
	* src/common/Events.ma (modified)

	Sort out cost labels.


Tue, 29 Mar 2011 15:54:37 GMT campbell [718]
	* src/Clight/AST.ma (modified)
	* src/Clight/Animation.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Values.ma (modified)

	Add an AST type (i.e., intermediate language type) for pointers.


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 11:30:38 GMT campbell [694]
	* src/Clight (moved)

	Start moving Clight into common directory.


Fri, 11 Feb 2011 15:45:36 GMT campbell [498]
	* Deliverables/D3.1/C-semantics/Cexec.ma (modified)
	* Deliverables/D3.1/C-semantics/CexecComplete.ma (modified)
	* Deliverables/D3.1/C-semantics/CexecSound.ma (modified)
	* Deliverables/D3.1/C-semantics/Csem.ma (modified)
	* Deliverables/D3.1/C-semantics/Csyntax.ma (modified)
	* Deliverables/D3.1/C-semantics/Globalenvs.ma (modified)
	* Deliverables/D3.1/C-semantics/Mem.ma (modified)
	* Deliverables/D3.1/C-semantics/Values.ma (modified)

	Make block type a little more abstract; remove knowledge about the ...