# # ChangeLog for src/utilities/extralib.ma # # Generated by Trac 1.2 # Apr 18, 2021, 1:53:32 AM Thu, 12 Jul 2012 12:56:50 GMT campbell [2178] * src/Cminor/toRTLabs.ma (modified) * src/utilities/extralib.ma (modified) Shift some notation into utilities. Tue, 19 Jun 2012 14:43:50 GMT boender [2101] * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) * src/utilities/extralib.ma (modified) - renamed medium to absolute jump - revised proofs of policy, some ... 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 ... Tue, 15 May 2012 15:51:25 GMT tranquil [1949] * src/common/Errors.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Identifiers.ma (modified) * src/common/StructuredTraces.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/blocks.ma (modified) * src/joint/semantics_blocks.ma (modified) * src/joint/semantics_paolo.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/monad.ma (modified) * src/utilities/option.ma (modified) * lemma trace rel to eq flatten trace * some more properties of ... Wed, 09 May 2012 16:30:41 GMT campbell [1930] * src/Clight/CexecComplete.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/common/IOMonad.ma (modified) * src/utilities/extralib.ma (modified) Tidy up labelling simulation stuff a bit. Fri, 06 Apr 2012 18:02:10 GMT tranquil [1882] * src/ASM/ASM.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/AST.ma (modified) * src/common/Errors.ma (modified) * src/common/Graphs.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Identifiers.ma (modified) * src/common/LabelledObjects.ma (added) * src/common/Pointers.ma (modified) * src/common/PositiveMap.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/blocks.ma (added) * src/joint/semanticsUtils_paolo.ma (modified) * src/joint/semantics_blocks.ma (added) * src/joint/semantics_paolo.ma (modified) * src/utilities/bindLists.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/monad.ma (modified) * src/utilities/option.ma (modified) * src/utilities/state.ma (modified) * src/utilities/trace.ma (modified) big update, alas incomplete: joint changed a bit, and all BE ... 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. Wed, 07 Dec 2011 14:48:32 GMT boender [1593] * src/ASM/Assembly.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) - cleaned up Assembly, moved some definitions elsewhere Mon, 21 Nov 2011 15:29:16 GMT campbell [1523] * src/common/Mem.ma (modified) * src/utilities/binary/Z.ma (modified) * src/utilities/binary/division.ma (added) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) Separate out positive and Z definitions from extralib.ma. Minor ... 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, 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 ... Tue, 11 Oct 2011 00:27:53 GMT sacerdot [1350] * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/common/AST.ma (modified) * src/utilities/extralib.ma (modified) Porting to latest destruct tactic. Note: the tactics has a few ... Mon, 10 Oct 2011 14:05:50 GMT sacerdot [1338] * src/utilities/extralib.ma (modified) Automation is now stronger. Mon, 10 Oct 2011 14:03:19 GMT sacerdot [1337] * src/utilities/extralib.ma (modified) Automation is now stronger. Fri, 07 Oct 2011 10:26:39 GMT campbell [1316] * src (modified) * src/ASM (modified) * src/ASM/BitVectorTrie.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/syntax.ma (modified) * src/common/Errors.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/deppair.ma (copied) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/option.ma (modified) * src/utilities/pair.ma (copied) Merge in id-lookup-branch to trunk. Fri, 23 Sep 2011 13:04:20 GMT mulligan [1260] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (modified) * src/joint/Joint.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/sigma.ma (added) commit for csc Thu, 22 Sep 2011 10:02:35 GMT sacerdot [1250] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) * src/utilities/extralib.ma (modified) 1. Sigma types projections moved to utilities/extralib.ma 2. ... Tue, 07 Jun 2011 14:53:53 GMT campbell [891] * src/ASM/BitVectorZ.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/common/Mem.ma (modified) * src/common/Smallstep.ma (modified) * src/common/Values.ma (modified) * src/utilities/binary/Z.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) Revise proofs affected by recent matita change. 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. Sun, 27 Mar 2011 13:06:13 GMT sacerdot [711] * src/utilities/extralib.ma (modified) ... Wed, 23 Mar 2011 15:39:01 GMT sacerdot [709] * src/utilities/extralib.ma (modified) Notations should NOT be redefined. Just add a new interpretation. 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 11:59:56 GMT campbell [695] * src/Clight/depends (deleted) * src/Clight/root (deleted) * src/RTLabs (moved) * src/common/Errors.ma (moved) * src/common/Events.ma (moved) * src/common/Floats.ma (moved) * src/common/FrontEndOps.ma (moved) * src/common/Globalenvs.ma (moved) * src/common/Graphs.ma (moved) * src/common/IOMonad.ma (moved) * src/common/Integers.ma (moved) * src/common/Maps.ma (moved) * src/common/Mem.ma (moved) * src/common/Registers.ma (moved) * src/common/Smallstep.ma (moved) * src/common/SmallstepExec.ma (moved) * src/common/Values.ma (moved) * src/utilities/Coqlib.ma (moved) * src/utilities/binary (moved) * src/utilities/extralib.ma (moved) Rearrange Clight files a bit - will try to make them work again soon... Fri, 18 Mar 2011 11:30:38 GMT campbell [694] * src/Clight (moved) Start moving Clight into common directory.