# # ChangeLog for src/RTLabs/import.ma # # Generated by Trac 1.2 # Apr 16, 2021, 12:21:51 PM Wed, 04 Jan 2012 18:19:09 GMT campbell [1633] * src/Clight/clightPrintMatita.ml (modified) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/factorial.Cminor.ma (added) * src/Cminor/test/factorial.ma (deleted) * src/Cminor/test/factorial.test.ma (added) * src/Cminor/test/null-op.Cminor.ma (modified) * src/Cminor/test/null-op.test.ma (added) * src/Cminor/test/search.Cminor.ma (modified) * src/Cminor/test/search.test.ma (modified) * src/Cminor/test/sum-bad.ma (deleted) * src/Cminor/test/switcher.ma (deleted) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/import.ma (modified) * src/acc-matita-printers.patch (modified) Update Cminor pretty printer and examples. Wed, 14 Dec 2011 14:58:39 GMT sacerdot [1612] * src/Clight/toCminor.ma (modified) * src/RTLabs/import.ma (modified) All library ported to new Matita lib (finally). 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. 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. 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. 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: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 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 ... 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 ... 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 ... Mon, 04 Apr 2011 15:13:10 GMT campbell [738] * src/Clight/AST.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/RTLabs/import.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Use lower case names for identifiers for consistency with CompCert ... Mon, 04 Apr 2011 15:13:08 GMT campbell [736] * src/RTLabs/RTLabs-sem.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (added) * src/common/Registers.ma (modified) Extra type safety for identifiers. Thu, 31 Mar 2011 15:20:00 GMT campbell [727] * src/RTLabs/RTLabs-sem.ma (modified) * src/RTLabs/import.ma (modified) * src/common/FrontEndOps.ma (modified) Enough fixes to let an RTLabs program run. Wed, 30 Mar 2011 16:47:35 GMT campbell [726] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/AST.ma (modified) * src/Clight/CexecComplete.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/RTLabs/import.ma (modified) * src/common/Graphs.ma (modified) * src/common/Registers.ma (modified) Change identifiers to Words in Clight and RTLabs semantics. Fri, 25 Mar 2011 17:37:49 GMT campbell [710] * src/RTLabs/import.ma (added) * src/common/Graphs.ma (modified) * src/common/Registers.ma (modified) Start of way to import RTLabs from prototype compiler.