# # ChangeLog for src/ASM/BitVector.ma # # Generated by Trac 1.2 # Feb 28, 2021, 3:03:30 PM Thu, 07 Feb 2013 20:22:22 GMT sacerdot [2645] * src/ASM/ASM.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Char.ma (deleted) * src/ASM/I8051.ma (modified) * src/BACKEND_BROKEN_FILES (added) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/test/addptrcharboth.test.ma (modified) * src/Clight/test/badconditional.test.ma (modified) * src/Clight/test/controlflow.test.ma (modified) * src/Clight/test/endptr.test.ma (modified) * src/Clight/test/endptr2.test.ma (modified) * src/Clight/test/forcont.test.ma (modified) * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/implicit.test.ma (modified) * src/Clight/test/implicitcond.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Clight/test/trivial.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/Cminor_semantics.ma (modified) * src/Cminor/Cminor_syntax.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTLptr/ERTLptr.ma (modified) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/LIN/joint_LTL_LIN.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/RTL/RTL_semantics.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/RTLabs/import.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/BackEndOps.ma (modified) * src/common/ByteValues.ma (modified) * src/common/CostLabel.ma (modified) * src/common/ErrorMessages.ma (added) * src/common/Errors.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Graphs.ma (modified) * src/common/IO.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PreIdentifiers.ma (modified) * src/common/Registers.ma (modified) * src/common/Values.ma (modified) * src/compiler.ma (modified) * src/joint/Joint.ma (modified) * src/joint/String.ma (moved) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) 1. some broken back-end files repaires, several still to go 2. the ... Tue, 05 Feb 2013 12:36:31 GMT sacerdot [2601] * extracted (added) * extracted/PROBLEMS (added) * extracted/aSM.ml (added) * extracted/aSM.mli (added) * extracted/aSMCosts.ml (added) * extracted/aSMCosts.mli (added) * extracted/aSMCostsSplit.ml (added) * extracted/aSMCostsSplit.mli (added) * extracted/aST.ml (added) * extracted/aST.mli (added) * extracted/abstractStatus.ml (added) * extracted/abstractStatus.mli (added) * extracted/arithmetic.ml (added) * extracted/arithmetic.mli (added) * extracted/bitVector.ml (added) * extracted/bitVector.mli (added) * extracted/bitVectorTrie.ml (added) * extracted/bitVectorTrie.mli (added) * extracted/bitVectorZ.ml (added) * extracted/bitVectorZ.mli (added) * extracted/bool.ml (added) * extracted/bool.mli (added) * extracted/byteValues.ml (added) * extracted/byteValues.mli (added) * extracted/casts.ml (added) * extracted/casts.mli (added) * extracted/cexec.ml (added) * extracted/cexec.mli (added) * extracted/cexecInd.ml (added) * extracted/cexecInd.mli (added) * extracted/cexecSound.ml (added) * extracted/cexecSound.mli (added) * extracted/char.ml (added) * extracted/char.mli (added) * extracted/classifyOp.ml (added) * extracted/classifyOp.mli (added) * extracted/cminor_syntax.ml (added) * extracted/cminor_syntax.mli (added) * extracted/compiler.ml (added) * extracted/compiler.mli (added) * extracted/coqlib.ml (added) * extracted/coqlib.mli (added) * extracted/core_notation.ml (added) * extracted/core_notation.mli (added) * extracted/costLabel.ml (added) * extracted/costLabel.mli (added) * extracted/csem.ml (added) * extracted/csem.mli (added) * extracted/csyntax.ml (added) * extracted/csyntax.mli (added) * extracted/deqsets.ml (added) * extracted/deqsets.mli (added) * extracted/div_and_mod.ml (added) * extracted/div_and_mod.mli (added) * extracted/division.ml (added) * extracted/division.mli (added) * extracted/errors.ml (added) * extracted/errors.mli (added) * extracted/events.ml (added) * extracted/events.mli (added) * extracted/extra_bool.ml (added) * extracted/extra_bool.mli (added) * extracted/extralib.ml (added) * extracted/extralib.mli (added) * extracted/extranat.ml (added) * extracted/extranat.mli (added) * extracted/fetch.ml (added) * extracted/fetch.mli (added) * extracted/floats.ml (added) * extracted/floats.mli (added) * extracted/foldStuff.ml (added) * extracted/foldStuff.mli (added) * extracted/fresh.ml (added) * extracted/fresh.mli (added) * extracted/frontEndMem.ml (added) * extracted/frontEndMem.mli (added) * extracted/frontEndOps.ml (added) * extracted/frontEndOps.mli (added) * extracted/frontEndVal.ml (added) * extracted/frontEndVal.mli (added) * extracted/frontend_misc.ml (added) * extracted/frontend_misc.mli (added) * extracted/genMem.ml (added) * extracted/genMem.mli (added) * extracted/globalenvs.ml (added) * extracted/globalenvs.mli (added) * extracted/graphs.ml (added) * extracted/graphs.mli (added) * extracted/hide.ml (added) * extracted/hide.mli (added) * extracted/hints_declaration.ml (added) * extracted/hints_declaration.mli (added) * extracted/iO.ml (added) * extracted/iO.mli (added) * extracted/iOMonad.ml (added) * extracted/iOMonad.mli (added) * extracted/identifiers.ml (added) * extracted/identifiers.mli (added) * extracted/initialisation.ml (added) * extracted/initialisation.mli (added) * extracted/integers.ml (added) * extracted/integers.mli (added) * extracted/interpret.ml (added) * extracted/interpret.mli (added) * extracted/jmeq.ml (added) * extracted/jmeq.mli (added) * extracted/label.ml (added) * extracted/label.mli (added) * extracted/labelledObjects.ml (added) * extracted/labelledObjects.mli (added) * extracted/list.ml (added) * extracted/list.mli (added) * extracted/listb.ml (added) * extracted/listb.mli (added) * extracted/lists.ml (added) * extracted/lists.mli (added) * extracted/logic.ml (added) * extracted/logic.mli (added) * extracted/memProperties.ml (added) * extracted/memProperties.mli (added) * extracted/memoryInjections.ml (added) * extracted/memoryInjections.mli (added) * extracted/monad.ml (added) * extracted/monad.mli (added) * extracted/nat.ml (added) * extracted/nat.mli (added) * extracted/option.ml (added) * extracted/option.mli (added) * extracted/order.ml (added) * extracted/order.mli (added) * extracted/pointers.ml (added) * extracted/pointers.mli (added) * extracted/positive.ml (added) * extracted/positive.mli (added) * extracted/positiveMap.ml (added) * extracted/positiveMap.mli (added) * extracted/preIdentifiers.ml (added) * extracted/preIdentifiers.mli (added) * extracted/preamble.ml (added) * extracted/proper.ml (added) * extracted/proper.mli (added) * extracted/pts.ml (added) * extracted/pts.mli (added) * extracted/rTLabs_syntax.ml (added) * extracted/rTLabs_syntax.mli (added) * extracted/registers.ml (added) * extracted/registers.mli (added) * extracted/relations.ml (added) * extracted/relations.mli (added) * extracted/russell.ml (added) * extracted/russell.mli (added) * extracted/setoids.ml (added) * extracted/setoids.mli (added) * extracted/sets.ml (added) * extracted/sets.mli (added) * extracted/simplifyCasts.ml (added) * extracted/simplifyCasts.mli (added) * extracted/smallstep.ml (added) * extracted/smallstep.mli (added) * extracted/smallstepExec.ml (added) * extracted/smallstepExec.mli (added) * extracted/star.ml (added) * extracted/star.mli (added) * extracted/status.ml (added) * extracted/status.mli (added) * extracted/statusProofs.ml (added) * extracted/statusProofs.mli (added) * extracted/string.ml (added) * extracted/string.mli (added) * extracted/structuredTraces.ml (added) * extracted/structuredTraces.mli (added) * extracted/switchRemoval.ml (added) * extracted/switchRemoval.mli (added) * extracted/toCminor.ml (added) * extracted/toCminor.mli (added) * extracted/toRTLabs.ml (added) * extracted/toRTLabs.mli (added) * extracted/typeComparison.ml (added) * extracted/typeComparison.mli (added) * extracted/types.ml (added) * extracted/types.mli (added) * extracted/util.ml (added) * extracted/util.mli (added) * extracted/utilBranch.ml (added) * extracted/utilBranch.mli (added) * extracted/values.ml (added) * extracted/values.mli (added) * extracted/vector.ml (added) * extracted/vector.mli (added) * extracted/z.ml (added) * extracted/z.mli (added) * src/ASM/BitVector.ma (modified) * src/Clight/Clight_abstract.ma (moved) * src/Clight/toCminor.ma (modified) * src/Clight/toCminorCorrectness.ma (modified) * src/Clight/toCminorCorrectnessExpr.ma (modified) * src/Clight/toCminorOps.ma (modified) * src/Cminor/Cminor_abstract.ma (moved) * src/Cminor/Cminor_semantics.ma (moved) * src/Cminor/Cminor_syntax.ma (moved) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/ERTL/ERTL_semantics.ma (moved) * src/ERTLptr/ERTLptr_semantics.ma (moved) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/LIN/LIN_semantics.ma (moved) * src/LTL/LTL_semantics.ma (moved) * src/RTL/RTL_semantics.ma (moved) * src/RTLabs/CostCheck.ma (modified) * src/RTLabs/CostInj.ma (modified) * src/RTLabs/CostSpec.ma (modified) * src/RTLabs/MeasurableTraces.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabs_abstract.ma (moved) * src/RTLabs/RTLabs_semantics.ma (moved) * src/RTLabs/RTLabs_syntax.ma (moved) * src/RTLabs/RTLabs_traces.ma (moved) * src/RTLabs/debug.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Globalenvs.ma (modified) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (moved) * src/joint/semanticsUtils.ma (modified) * src/joint/stacksize.ma (modified) * src/utilities/extra_bool.ma (moved) Extraction to ocaml is now working, with a couple of bugs left. One ... Wed, 27 Jun 2012 14:56:52 GMT sacerdot [2126] * src/ASM/BitVector.ma (modified) Proof improved (for case 3) + new proof (for case 11) Wed, 27 Jun 2012 14:23:54 GMT sacerdot [2124] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) Much more shuffling around to proper places Wed, 27 Jun 2012 13:36:54 GMT sacerdot [2122] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Vector.ma (modified) More stuff moved around in proper places Wed, 27 Jun 2012 13:30:58 GMT sacerdot [2121] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Vector.ma (modified) More functions moved to the places they belong to Wed, 30 May 2012 16:43:02 GMT boender [2006] * src/ASM/BitVector.ma (modified) * src/utilities/extralib.ma (modified) - added alias for bitvector zero - changed extralib bounded ... Wed, 09 May 2012 11:36:35 GMT mulligan [1928] * src/ASM/ASMCosts.ma (modified) * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/UtilBranch.ma (added) * src/common/Identifiers.ma (modified) Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should ... Wed, 18 Apr 2012 12:01:46 GMT boender [1890] * src/ASM/BitVector.ma (modified) - added comment about bitvector translation Fri, 06 Jan 2012 23:33:17 GMT tranquil [1635] * Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml (modified) * src/ASM/BitVector.ma (modified) * src/ASM/I8051.ma (modified) * src/RTL/RTL_paolo.ma (added) * src/RTLabs/RTLabsToRTL_paolo.ma (added) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/joint/Joint_paolo.ma (added) * src/joint/TranslateUtils_paolo.ma (added) * src/utilities/bindLists.ma (added) * src/utilities/monad.ma (added) * src/utilities/option.ma (added) * src/utilities/proper.ma (added) * src/utilities/setoids.ma (added) * src/utilities/state.ma (added) * src/utilities/trace.ma (added) * lists with binders and monads * Joint.ma and other temprarily ... 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. Mon, 21 Nov 2011 12:06:01 GMT sacerdot [1521] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Status.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/Z.ma (modified) Syntax change in Matita: change what where => change where what. Fri, 18 Nov 2011 23:38:20 GMT sacerdot [1516] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/BitVectorZ.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.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/casts.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/common/AST.ma (modified) * src/common/Events.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/GenMem.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Integers.ma (modified) * src/common/Mem.ma (modified) * src/common/Pointers.ma (modified) * src/common/PositiveMap.ma (modified) * src/joint/BEValues.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) * src/utilities/lists.ma (modified) Ported to syntax of Matita 0.99.1. Fri, 17 Jun 2011 11:30:01 GMT sacerdot [990] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/FoldStuff.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) Do no longer use the daemon automatically :-) Thu, 16 Jun 2011 14:50:23 GMT sacerdot [985] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/common/AST.ma (modified) 1) Major refactoring: proofs moved where they should be. 2) New ... 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 ... Tue, 31 May 2011 15:28:12 GMT mulligan [868] * src/ASM/AssemblyProof.ma (modified) * src/ASM/BitVector.ma (modified) more changes 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 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. Wed, 30 Mar 2011 12:03:05 GMT campbell [724] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/I8051.ma (modified) More tractable version of bitvector_of_nat / nat_of_bitvector. 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 12:47:53 GMT mulligan [698] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/String.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/utilities/BitVectorTrieSet.ma (modified) * src/utilities/StringTools.ma (modified) Commit with changes to files to get our files to typecheck. Fri, 18 Mar 2011 12:28:33 GMT campbell [697] * src/ASM (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/BitVectorZ.ma (copied) * src/ASM/Char.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/common/Integers.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/binary/Z.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/oldlib (moved) Merge Clight branch of vectors and friends. Start making stuff build. Fri, 18 Mar 2011 10:34:13 GMT mulligan [690] * src/ASM/ASM.ma (copied) * src/ASM/Arithmetic.ma (copied) * src/ASM/BitVector.ma (copied) * src/ASM/BitVectorTrie.ma (copied) * src/ASM/Char.ma (copied) * src/ASM/Fetch.ma (copied) * src/ASM/Interpret.ma (copied) * src/ASM/Status.ma (copied) * src/ASM/String.ma (copied) * src/ASM/Util.ma (copied) * src/ASM/Vector.ma (copied) * src/ASM/new-matita-development (deleted) Moved new matita files into correct place. Fri, 18 Mar 2011 10:31:32 GMT mulligan [688] * Deliverables/D4.1/Demo-March-2011 (deleted) * Deliverables/D4.2-4.3/LIN/LinToAsm.ma (deleted) * src (added) * src/ASM (moved) * src/LIN (moved) * src/LIN/LIN.ma (copied) Fixed local conflicts. Restructured svn repository.