#
# ChangeLog for src/common/extraGlobalenvs.ma
#
# Generated by Trac 1.2
# Mar 3, 2021, 1:22:45 AM

Wed, 06 Mar 2013 11:09:52 GMT piccolo [2783]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTL_semantics.ma (modified)
	* src/ERTL/ERTLtoERTLptrOK.ma (modified)
	* src/ERTLptr/ERTLptr.ma (modified)
	* src/ERTLptr/ERTLptr_semantics.ma (modified)
	* src/LIN/LIN_semantics.ma (modified)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/LTL/LTL_semantics.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/common/ExtraIdentifiers.ma (added)
	* src/common/ExtraMonads.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/extra_joint_semantics.ma (added)
	* src/joint/joint_semantics.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	modified joint_closed_internal_function definition (added condition ...


Wed, 06 Feb 2013 12:01:34 GMT garnier [2608]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/MemProperties.ma (modified)
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Clight/toCminorCorrectnessExpr.ma (modified)
	* src/Clight/toCminorOps.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/extraGlobalenvs.ma (modified)

	Regions are no more stored in blocks. block_region now tests the id, ...


Thu, 24 Jan 2013 18:52:38 GMT piccolo [2590]
	* src/ERTL/semantics.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/ERTLptr/semantics.ma (modified)
	* src/common/ExtraMonads.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/semantics.ma (modified)

	added monad machineary for ERTL to ERTLptr translation ...


Sat, 05 Jan 2013 12:41:13 GMT piccolo [2570]
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (added)
	* src/common/ExtraMonads.ma (added)
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/lineariseProof.ma (modified)
	* src/joint/semantics.ma (modified)

	ERTLtoERTLptr in place


Tue, 20 Nov 2012 13:28:06 GMT tranquil [2478]
	* src/common/extraGlobalenvs.ma (modified)

	unified is_internal_function_of_program and is_internal_function


Mon, 19 Nov 2012 17:04:24 GMT piccolo [2476]
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/lineariseProof.ma (modified)

	fixed commutation lemmas in lineariseProof
	started proof of main ...


Mon, 19 Nov 2012 09:57:08 GMT tranquil [2474]
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/linearise.ma (modified)

	changed form of a statement


Fri, 16 Nov 2012 17:59:24 GMT tranquil [2473]
	* src/common/extraGlobalenvs.ma (added)
	* src/joint/Traces.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)

	put some generic stuff we need in the back end in extraGlobalenvs ...