#
# ChangeLog for src/Clight/Csyntax.ma
#
# Generated by Trac 1.2
# Jan 21, 2021, 10:50:03 PM

Wed, 04 Apr 2012 16:48:23 GMT campbell [1872]
	* src/Clight/ClassifyOp.ma (added)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/TypeComparison.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/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Values.ma (modified)

	Make binary operations in Cminor/RTLabs properly typed.
	A few extra ...


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


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


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.


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