# # ChangeLog for src/ASM/Interpret.ma # # Generated by Trac 1.2 # Dec 7, 2019, 9:07:00 PM Tue, 19 Mar 2013 08:54:38 GMT sacerdot [2906] * src/ASM/Interpret.ma (modified) Bug fixed. Mon, 18 Mar 2013 23:33:13 GMT sacerdot [2899] * src/ASM/ASMCosts.ma (modified) * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/AbstractStatus.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/compiler.ma (modified) * src/semantics.ma (modified) 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system ... Sun, 03 Mar 2013 20:58:28 GMT mckinna [2770] * src/ASM/ASMCosts.ma (modified) * src/ASM/AbstractStatus.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/utilities/option.ma (modified) WARNING: another big commit, touching many files in ASM/*.ma This ... Sat, 02 Mar 2013 00:29:41 GMT sacerdot [2760] * src/ASM/ASM.ma (modified) * src/ASM/ASMCosts.ma (modified) * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/LIN/LINToASM.ma (modified) * src/RTLabs/MeasurableTraces.ma (modified) * src/RTLabs/RTLabs_traces.ma (modified) * src/common/StructuredTraces.ma (modified) * src/joint/semantics_blocks.ma (modified) 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in ... Fri, 01 Mar 2013 12:05:21 GMT sacerdot [2756] * src/ASM/ASMCosts.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/common/Measurable.ma (modified) * src/common/StatusSimulation.ma (modified) * src/common/StructuredTraces.ma (modified) WARNING: this commit breaks things, sorry, Paolo is going to fix ... Fri, 22 Feb 2013 16:56:31 GMT sacerdot [2705] * src/ASM/ASM.ma (modified) * src/ASM/AbstractStatus.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/Interpret.ma (modified) * src/BACKEND_BROKEN_FILES (modified) * src/compiler.ma (modified) More progress in ASM towards implementing the new pseudoinstructions. Thu, 29 Nov 2012 14:33:59 GMT mckinna [2504] * src/ASM/ASMCosts.ma (modified) * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/Interpret.ma (modified) More refactoring to support the tidied up compiler.ma Tue, 31 Jul 2012 16:11:27 GMT mulligan [2283] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) Work from today. Mon, 30 Jul 2012 22:10:59 GMT sacerdot [2280] * src/ASM/Interpret.ma (modified) Proof repaired. Mon, 30 Jul 2012 21:44:50 GMT sacerdot [2279] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Test.ma (modified) 1. Bug fixed in the semantics of PUSH (no indirection performed) 2. ... Fri, 27 Jul 2012 15:53:25 GMT mulligan [2272] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/StatusProofsSplit.ma (modified) * src/ASM/Test.ma (modified) Changed proof strategy for main lemma after noticed that the current ... Wed, 25 Jul 2012 22:38:42 GMT sacerdot [2264] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) * src/ASM/Status.ma (modified) 1) Major change: we now always use the efficient way of resolving ... Wed, 18 Jul 2012 15:30:26 GMT mulligan [2212] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) More work on the INC case Fri, 06 Jul 2012 15:26:21 GMT mulligan [2160] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Test.ma (added) Added a new scratch file Test.ma for working on lemmas that are ... Wed, 27 Jun 2012 20:19:57 GMT sacerdot [2130] * src/ASM/Interpret.ma (modified) Proof repaired after Dominic's bug fix. Wed, 27 Jun 2012 17:14:32 GMT mulligan [2129] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/common/StructuredTraces.ma (modified) Large changes from today trying to complete the main theorem. Again :( 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 Mon, 25 Jun 2012 12:39:06 GMT mulligan [2108] * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) Various axioms closed and others moved around. Uncommented main ... Wed, 13 Jun 2012 15:00:35 GMT sacerdot [2062] * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) Everything repaired (broken because of new proof obligation for fetch). Wed, 13 Jun 2012 11:01:05 GMT sacerdot [2056] * src/ASM/Interpret.ma (modified) Repaired, ported to new fetch_pseudo_assembly. The execute_n is ... Tue, 12 Jun 2012 15:49:02 GMT mulligan [2051] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) Finished the Jmp case in the main theorem. Tue, 12 Jun 2012 12:18:16 GMT mulligan [2047] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/PolicyFront.ma (modified) Big bugs in policy calculations found. Waiting for Jaap's commit. Fri, 08 Jun 2012 17:38:12 GMT sacerdot [2040] * src/ASM/Interpret.ma (modified) Repaired using new /demod/ that allows to specify the rules to be used. Fri, 08 Jun 2012 15:52:23 GMT sacerdot [2036] * src/ASM/Interpret.ma (modified) New daemon inserted because /demod/ got worst :-( Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ASM/WellLabeled.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/casts.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) !! BEWARE: major commit !! 1) [affects everybody] split for ... Sat, 02 Jun 2012 20:39:35 GMT mulligan [2014] * src/ASM/Interpret.ma (modified) Fixed problem in James' email message. Sun, 20 May 2012 20:34:31 GMT sacerdot [1971] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) 1. Interpret.ma: we need to prove \sigma ... Fri, 18 May 2012 16:14:01 GMT sacerdot [1969] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) Some more progress, but now we must prove something on a Russell ... Thu, 17 May 2012 10:06:34 GMT tranquil [1964] * src/ASM/ASMCosts.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Util.ma (modified) * src/common/StructuredTraces.ma (modified) introduced as_label_of_cost and adapted accordingly. Equality of cost ... Wed, 16 May 2012 22:25:41 GMT sacerdot [1962] * src/ASM/ASMCosts.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/StatusProofs.ma (modified) More examples are now indexed. Tue, 15 May 2012 23:28:43 GMT sacerdot [1951] * src/ASM/Interpret.ma (modified) Bug with overloaded names in the context. Tue, 15 May 2012 09:13:14 GMT mulligan [1948] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so ... Mon, 14 May 2012 22:01:30 GMT sacerdot [1946] * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/UtilBranch.ma (modified) \snd half_add => add everywhere Mon, 14 May 2012 08:37:08 GMT mulligan [1939] * src/ASM/AbstractStatus.ma (added) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/common/StructuredTraces.ma (modified) Changes to get things to compile and to avoid the dependency ... Mon, 14 May 2012 08:05:36 GMT sacerdot [1938] * src/ASM/ASMCosts.ma (modified) * src/ASM/Interpret.ma (modified) * src/common/StructuredTraces.ma (modified) Definitions moved to the right places, now everything compiles again. Thu, 10 May 2012 15:13:34 GMT mulligan [1935] * src/ASM/ASMCosts.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/common/StructuredTraces.ma (modified) Generalized some lemma in ASM/CostsProof.ma to work on abstract ... 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 ... Fri, 27 Apr 2012 15:48:20 GMT mulligan [1910] * src/ASM/ASMCosts.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) Finished proof modulo termination argument Fri, 27 Apr 2012 08:59:03 GMT mulligan [1909] * src/ASM/ASMCosts.ma (modified) * src/ASM/Interpret.ma (modified) Ported new statements to remainder of Interpret.ma file. Mon, 20 Feb 2012 09:04:54 GMT mulligan [1710] * src/ASM/ASMCosts.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/StatusProofs.ma (modified) changes from friday afternoon Fri, 17 Feb 2012 10:52:36 GMT mulligan [1709] * src/ASM/ASMCosts.ma (modified) * src/ASM/Interpret.ma (modified) * src/common/StructuredTraces.ma (modified) * src/joint/semantics_paolo.ma (modified) Changes to the execution of the MOVC instruction Sat, 28 Jan 2012 12:42:15 GMT sacerdot [1666] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) PreStatus datatype change: the code_memory field is not a left ... Wed, 14 Dec 2011 12:40:08 GMT sacerdot [1606] * src/ASM/ASMCosts.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/ASM/StatusProofs.ma (modified) Porting to last library of Matita. Tue, 13 Dec 2011 12:41:08 GMT sacerdot [1600] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/FoldStuff.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/JMCoercions.ma (deleted) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/utilities/Compare.ma (deleted) * src/utilities/Coqlib.ma (modified) * src/utilities/deppair.ma (deleted) * src/utilities/lists.ma (deleted) * src/utilities/option.ma (deleted) * src/utilities/sigma.ma (deleted) utilities and ASM ported to the new standard library Tue, 06 Dec 2011 10:21:37 GMT sacerdot [1588] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) All goals generated by Russell for execute_1* are now closed, mostly ... Mon, 05 Dec 2011 16:16:55 GMT mulligan [1587] * src/ASM/ASMCosts.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/utilities/binary/positive.ma (modified) changes from today, including removing indexing of problematic ... Thu, 01 Dec 2011 16:24:41 GMT mulligan [1582] * src/ASM/Interpret.ma (modified) more added to the proof of execute_1_preinstruction --- ~260 cases ... Thu, 01 Dec 2011 14:15:15 GMT mulligan [1581] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) Dangling de Bruijn pointer when trying to propagate russell to set_arg_1 Wed, 30 Nov 2011 16:32:52 GMT mulligan [1577] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) A lot more cases added to the proof at the bottom of ... Tue, 29 Nov 2011 13:21:39 GMT mulligan [1575] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) Changes to specifications on execute functions Mon, 28 Nov 2011 16:13:04 GMT mulligan [1573] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) more complicated than it appears :( Wed, 23 Nov 2011 22:08:42 GMT sacerdot [1547] * src/ASM/Interpret.ma (modified) Invariant on cost of one execution step strengthened. Wed, 23 Nov 2011 15:31:01 GMT mulligan [1541] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) interpret.ma now compiles Wed, 23 Nov 2011 15:03:38 GMT mulligan [1540] * src/ASM/Interpret.ma (modified) changes to proof in interrupt.ma Wed, 23 Nov 2011 11:28:51 GMT mulligan [1538] * src/ASM/Interpret.ma (modified) changes to execute_1_0 proof Wed, 23 Nov 2011 09:36:34 GMT mulligan [1534] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) committing my changes to interpret to prevent any further conflicts Tue, 22 Nov 2011 18:24:00 GMT sacerdot [1533] * src/ASM/Interpret.ma (modified) Proof of execute_1 with Russell completed (up to some daemon used ... Tue, 22 Nov 2011 10:50:15 GMT sacerdot [1527] * src/ASM/Interpret.ma (modified) More on Russell. Tue, 22 Nov 2011 09:43:47 GMT sacerdot [1526] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) Using Russell to prove some properties. Mon, 21 Nov 2011 14:49:04 GMT mulligan [1522] * src/ASM/ASM.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/LIN/LINToASM.ma (modified) changes to preamble and lin to asm pass, resolved conflict in interpret Mon, 21 Nov 2011 11:10:57 GMT campbell [1519] * src/ASM/Interpret.ma (modified) * src/ASM/StatusProofs.ma (modified) More syntax updates. Fri, 18 Nov 2011 12:03:14 GMT campbell [1515] * src/ASM/ASM.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/fresh.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/insertsort.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PositiveMap.ma (added) * src/common/PreIdentifiers.ma (modified) * src/joint/Erasure.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) Add type of maps on positive binary numbers, and use them for ... Thu, 17 Nov 2011 16:41:08 GMT mulligan [1514] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) changes from today. matita keeps dieing Wed, 16 Nov 2011 16:35:24 GMT mulligan [1511] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) proofs, added, changes to execute_1_0 function therefore required to ... Mon, 07 Nov 2011 09:56:13 GMT mulligan [1494] * src/ASM/Interpret.ma (modified) * src/ASM/WellLabeled.ma (modified) changes to get everything compiling again Thu, 23 Jun 2011 00:56:20 GMT sacerdot [1037] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Main theorem: comments are working again. 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 ... Fri, 10 Jun 2011 14:20:47 GMT sacerdot [936] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Ticks are now handled correctly everywhere and the main proof takes ... Thu, 09 Jun 2011 16:07:29 GMT sacerdot [928] * src/ASM/Interpret.ma (modified) Technical splitting. Thu, 09 Jun 2011 08:36:35 GMT mulligan [910] * src/ASM/Interpret.ma (modified) removed bug in execute_1_pseudoinstruction Tue, 31 May 2011 09:45:21 GMT sacerdot [865] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Renaming. Mon, 30 May 2011 11:44:45 GMT sacerdot [856] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Util.ma (modified) 1. if_then_else is now a notation for match with (to allow Russell to ... Wed, 25 May 2011 13:57:42 GMT sacerdot [843] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) Function moved from Interpret to Status. Tue, 24 May 2011 11:26:43 GMT sacerdot [827] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) The preamble is now part of the PseudoStatus. Mon, 23 May 2011 16:12:51 GMT mulligan [825] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) lots of refactoring, finally got something to prove Mon, 23 May 2011 14:22:13 GMT mulligan [822] * src/ASM/Interpret.ma (modified) removed all axioms Mon, 23 May 2011 13:23:17 GMT mulligan [821] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) changes to introduce pseudostatus Fri, 20 May 2011 16:09:00 GMT mulligan [820] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) changes to get the semantics of pseudoassembly working Mon, 18 Apr 2011 10:30:53 GMT mulligan [757] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Lots more fixing to get both front and backends using same ... Mon, 28 Mar 2011 15:40:51 GMT mulligan [712] * src/ASM/Arithmetic.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Util.ma (modified) Changes to get things to typecheck. 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 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.