Commit 864394e7 authored by root's avatar root

update

parent 1297995b
theory cic:/DiSeL?Actions
HasMeta cic:/DiSeL?Actions http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Actions cic:/Coq/Logic?Classical_Prop
Includes cic:/DiSeL?Actions cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Actions cic:/DiSeL?Worlds
Includes cic:/DiSeL?Actions cic:/DiSeL?Protocols
Includes cic:/DiSeL?Actions cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?Actions cic:/DiSeL?State
Includes cic:/DiSeL?Actions cic:/DiSeL?Freshness
Includes cic:/DiSeL?Actions cic:/fcsl/pcm?heap
Includes cic:/DiSeL?Actions cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Actions cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Actions cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?Actions cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Actions cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?Actions cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Actions cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?Actions cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?Actions cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?Actions http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/DiSeL?Actions cic:/DiSeL?Actions?Actions
theory cic:/DiSeL?Actions/Actions
HasMeta cic:/DiSeL?Actions/Actions http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Freshness
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Protocols/Transitions
Includes cic:/DiSeL?Actions/Actions cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Actions/Actions cic:/Coq/Logic?Classical_Prop
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Protocols/Transitions/Exports
Includes cic:/DiSeL?Actions/Actions cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?heap/Heap/Exports
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Protocols
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?heap/Heap
Includes cic:/DiSeL?Actions/Actions cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Actions/Actions cic:/Coq/Init?Logic
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Actions/Actions cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?State
Includes cic:/DiSeL?Actions/Actions cic:/DiSeL?Worlds/WorldGetters
Declares cic:/DiSeL?Actions/Actions cic:/DiSeL?Actions/Actions?Actions
deriveddeclaration cic:/DiSeL?Actions/Actions?Actions
Declares cic:/DiSeL?Actions/Actions cic:/DiSeL?Actions/Actions?a_safe
......@@ -82,10 +117,25 @@ Includes cic:/DiSeL?Actions cic:/DiSeL?Actions/Actions
Declares cic:/DiSeL?Actions cic:/DiSeL?Actions?ActionExports
theory cic:/DiSeL?Actions/ActionExports
HasMeta cic:/DiSeL?Actions/ActionExports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Actions/ActionExports cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Actions/ActionExports cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?Actions/ActionExports cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Protocols/Transitions/Exports
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Protocols
Includes cic:/DiSeL?Actions/ActionExports cic:/fcsl/pcm?heap/Heap
Includes cic:/DiSeL?Actions/ActionExports cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Actions/ActionExports cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Actions/ActionExports cic:/Coq/Init?Logic
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Actions/ActionExports cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?State
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Actions/Actions
Includes cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Worlds/WorldGetters
Declares cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Actions/ActionExports?action
constant cic:/DiSeL?Actions/ActionExports?action
Declares cic:/DiSeL?Actions/ActionExports cic:/DiSeL?Actions/ActionExports?a_safe
......
......@@ -37,17 +37,46 @@ dataconstructor cic:/DiSeL?Always?alw_inject
dataconstructor cic:/DiSeL?Always?aft_inject
theory cic:/DiSeL?Always
HasMeta cic:/DiSeL?Always http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Always cic:/fcsl/pcm?pcm/CancellativePCM
Includes cic:/DiSeL?Always cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?Always cic:/fcsl/pcm?pcm/CancellativePCM/Exports
Includes cic:/DiSeL?Always cic:/Coq/Classes?Morphisms_Prop
Includes cic:/DiSeL?Always cic:/Coq/Program?Basics
Includes cic:/DiSeL?Always cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?Always cic:/Coq/Classes?RelationClasses
Includes cic:/DiSeL?Always cic:/Coq/Classes?Morphisms
Includes cic:/DiSeL?Always cic:/DiSeL?InductiveInv/PWIExports
Includes cic:/DiSeL?Always cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Always cic:/DiSeL?Injection/Injection/Exports
Includes cic:/DiSeL?Always cic:/DiSeL?Actions/Actions
Includes cic:/DiSeL?Always cic:/DiSeL?Actions/ActionExports
Includes cic:/DiSeL?Always cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Always cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Always cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Always cic:/Coq/Init?Logic
Includes cic:/DiSeL?Always cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Always cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Always cic:/DiSeL?Worlds/WorldGetters
Includes cic:/DiSeL?Always cic:/DiSeL?InductiveInv
Includes cic:/DiSeL?Always cic:/DiSeL?Process
Includes cic:/DiSeL?Always cic:/DiSeL?Injection
Includes cic:/DiSeL?Always cic:/DiSeL?Actions
Includes cic:/DiSeL?Always cic:/DiSeL?Rely
Includes cic:/DiSeL?Always cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Always cic:/DiSeL?Worlds
Includes cic:/DiSeL?Always cic:/DiSeL?Protocols
Includes cic:/DiSeL?Always cic:/DiSeL?DepMaps
Includes cic:/DiSeL?Always cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?Always cic:/DiSeL?State
Includes cic:/DiSeL?Always cic:/DiSeL?Freshness
Includes cic:/DiSeL?Always cic:/fcsl/pcm?heap
Includes cic:/DiSeL?Always cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Always cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Always cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?Always cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Always cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?Always cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Always cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?Always cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?Always cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?Always http://coq.inria.fr/foundation?CoqSyntax
......@@ -133,10 +162,21 @@ Declares cic:/DiSeL?Always cic:/DiSeL?Always?AlwaysInductiveInv
theory cic:/DiSeL?Always/AlwaysInductiveInv
HasMeta cic:/DiSeL?Always/AlwaysInductiveInv http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Injection/Injection/Exports
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Actions/ActionExports
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Rely
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Worlds/WorldGetters
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/Coq/Init?Logic
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Process
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?InductiveInv/PWIExports
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?State
Includes cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Protocols/Protocols/Exports
Declares cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Always/AlwaysInductiveInv?AlwaysInductiveInv
deriveddeclaration cic:/DiSeL?Always/AlwaysInductiveInv?AlwaysInductiveInv
Declares cic:/DiSeL?Always/AlwaysInductiveInv cic:/DiSeL?Always/AlwaysInductiveInv?alw_ind_inv
......
theory cic:/DiSeL?DepMaps
HasMeta cic:/DiSeL?DepMaps http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?DepMaps cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?DepMaps cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?DepMaps cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?DepMaps cic:/DiSeL?Freshness
Includes cic:/DiSeL?DepMaps cic:/fcsl/pcm?heap
Includes cic:/DiSeL?DepMaps cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?DepMaps cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?DepMaps cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?DepMaps cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?DepMaps cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?DepMaps cic:/fcsl/pcm?pred
Includes cic:/DiSeL?DepMaps http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?DepMaps cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?DepMaps cic:/Coq/Relations?Relation_Operators
Declares cic:/DiSeL?DepMaps cic:/DiSeL?DepMaps?DepMaps
theory cic:/DiSeL?DepMaps/DepMaps
HasMeta cic:/DiSeL?DepMaps/DepMaps http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?DepMaps/DepMaps cic:/Coq/Init?Logic
Includes cic:/DiSeL?DepMaps/DepMaps cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?DepMaps/DepMaps cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?DepMaps/DepMaps cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?DepMaps/DepMaps cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?DepMaps
deriveddeclaration cic:/DiSeL?DepMaps/DepMaps?DepMaps
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?Label
constant cic:/DiSeL?DepMaps/DepMaps?Label
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?dmDom
constant cic:/DiSeL?DepMaps/DepMaps?dmDom
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?dmap
constant cic:/DiSeL?DepMaps/DepMaps?dmap
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?pf
constant cic:/DiSeL?DepMaps/DepMaps?pf
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?dmDom_unit
constant cic:/DiSeL?DepMaps/DepMaps?dmDom_unit
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?unit
constant cic:/DiSeL?DepMaps/DepMaps?unit
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?dmDom_join
constant cic:/DiSeL?DepMaps/DepMaps?dmDom_join
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?join
constant cic:/DiSeL?DepMaps/DepMaps?join
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?valid
constant cic:/DiSeL?DepMaps/DepMaps?valid
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?PCMLaws
deriveddeclaration cic:/DiSeL?DepMaps/DepMaps?PCMLaws
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?joinC
constant cic:/DiSeL?DepMaps/DepMaps?joinC
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?joinCA
constant cic:/DiSeL?DepMaps/DepMaps?joinCA
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?joinA
constant cic:/DiSeL?DepMaps/DepMaps?joinA
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?validL
constant cic:/DiSeL?DepMaps/DepMaps?validL
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?unitL
constant cic:/DiSeL?DepMaps/DepMaps?unitL
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?validU
constant cic:/DiSeL?DepMaps/DepMaps?validU
Declares cic:/DiSeL?DepMaps/DepMaps cic:/DiSeL?DepMaps/DepMaps?Exports
theory cic:/DiSeL?DepMaps/DepMaps/Exports
HasMeta cic:/DiSeL?DepMaps/DepMaps/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/Coq/Init?Logic
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?DepMaps/DepMaps/Exports cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/DiSeL?DepMaps/DepMaps/Exports cic:/DiSeL?DepMaps/DepMaps/Exports?Exports
deriveddeclaration cic:/DiSeL?DepMaps/DepMaps/Exports?Exports
Declares cic:/DiSeL?DepMaps/DepMaps/Exports cic:/DiSeL?DepMaps/DepMaps/Exports?depmap
......
theory cic:/DiSeL?DiSeLExtraction
HasMeta cic:/DiSeL?DiSeLExtraction http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?DiSeLExtraction cic:/Coq/extraction?ExtrOcamlBasic
Includes cic:/DiSeL?DiSeLExtraction http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?DiSeLExtraction cic:/DiSeL?While
......@@ -212,6 +212,9 @@ Includes cic:/DiSeL?Domain cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Domain cic:/Coq/Init?Logic
Includes cic:/DiSeL?Domain cic:/Coq/Init?Specif
Includes cic:/DiSeL?Domain cic:/DiSeL?Domain/Poset/Exports
Includes cic:/DiSeL?Domain cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?Domain cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Domain cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?Domain http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/DiSeL?Domain cic:/DiSeL?Domain?Poset
theory cic:/DiSeL?Domain/Poset
......@@ -359,6 +362,7 @@ Declares cic:/DiSeL?Domain cic:/DiSeL?Domain?Lattice
theory cic:/DiSeL?Domain/Lattice
HasMeta cic:/DiSeL?Domain/Lattice http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Domain/Lattice cic:/Coq/ssr?ssrfun
Includes cic:/DiSeL?Domain/Lattice cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Domain/Lattice cic:/DiSeL?Domain/Poset
Declares cic:/DiSeL?Domain/Lattice cic:/DiSeL?Domain/Lattice?RawMixin
deriveddeclaration cic:/DiSeL?Domain/Lattice?RawMixin
......@@ -386,6 +390,7 @@ Declares cic:/DiSeL?Domain/Lattice cic:/DiSeL?Domain/Lattice?Exports
theory cic:/DiSeL?Domain/Lattice/Exports
HasMeta cic:/DiSeL?Domain/Lattice/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Domain/Lattice/Exports cic:/DiSeL?Domain/Poset
Includes cic:/DiSeL?Domain/Lattice/Exports cic:/fcsl/pcm?pred
Declares cic:/DiSeL?Domain/Lattice/Exports cic:/DiSeL?Domain/Lattice/Exports?Laws
deriveddeclaration cic:/DiSeL?Domain/Lattice/Exports?Laws
Declares cic:/DiSeL?Domain/Lattice/Exports cic:/DiSeL?Domain/Lattice/Exports?supP
......@@ -606,6 +611,7 @@ Declares cic:/DiSeL?Domain cic:/DiSeL?Domain?CPO
theory cic:/DiSeL?Domain/CPO
HasMeta cic:/DiSeL?Domain/CPO http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Domain/CPO cic:/Coq/ssr?ssrfun
Includes cic:/DiSeL?Domain/CPO cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Domain/CPO cic:/DiSeL?Domain/Poset
Declares cic:/DiSeL?Domain/CPO cic:/DiSeL?Domain/CPO?RawMixin
deriveddeclaration cic:/DiSeL?Domain/CPO?RawMixin
......@@ -636,6 +642,7 @@ constant cic:/DiSeL?Domain/CPO?bot
Declares cic:/DiSeL?Domain/CPO cic:/DiSeL?Domain/CPO?Exports
theory cic:/DiSeL?Domain/CPO/Exports
HasMeta cic:/DiSeL?Domain/CPO/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Domain/CPO/Exports cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Domain/CPO/Exports cic:/DiSeL?Domain/Poset
Declares cic:/DiSeL?Domain/CPO/Exports cic:/DiSeL?Domain/CPO/Exports?Laws
deriveddeclaration cic:/DiSeL?Domain/CPO/Exports?Laws
......@@ -805,6 +812,7 @@ Includes cic:/DiSeL?Domain/Kleene cic:/Coq/Classes?Morphisms
Includes cic:/DiSeL?Domain/Kleene cic:/DiSeL?Domain/CPO/Exports
Includes cic:/DiSeL?Domain/Kleene cic:/DiSeL?Domain/Poset/Exports
Includes cic:/DiSeL?Domain/Kleene cic:/DiSeL?Domain/CPO
Includes cic:/DiSeL?Domain/Kleene cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Domain/Kleene cic:/DiSeL?Domain/Poset
Includes cic:/DiSeL?Domain/Kleene cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Domain/Kleene cic:/Coq/Init?Logic
......
......@@ -4,44 +4,20 @@ dataconstructor cic:/DiSeL?EqTypeX?eqMixinX
dataconstructor cic:/DiSeL?EqTypeX?eqTypeX'
theory cic:/DiSeL?EqTypeX
HasMeta cic:/DiSeL?EqTypeX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?EqTypeX cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?EqTypeX cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?EqTypeX cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?EqTypeX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?EqTypeX cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?EqTypeX cic:/Coq/Relations?Relation_Operators
Declares cic:/DiSeL?EqTypeX cic:/DiSeL?EqTypeX?EqualityX
theory cic:/DiSeL?EqTypeX/EqualityX
HasMeta cic:/DiSeL?EqTypeX/EqualityX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/ssr?ssrfun
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Init?Logic/EqNotations
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Init?Logic
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Bool?Bool
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Init?Notations/IfNotations
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Init?Notations
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Init?Specif
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/ssr?ssrbool/DefaultKeying
Includes cic:/DiSeL?EqTypeX/EqualityX cic:/Coq/ssr?ssrbool
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?axiom
constant cic:/DiSeL?EqTypeX/EqualityX?axiom
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?mixin_of_DEF
deriveddeclaration cic:/DiSeL?EqTypeX/EqualityX?mixin_of_DEF
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?mixin_of
constant cic:/DiSeL?EqTypeX/EqualityX?mixin_of
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?Mixin
constant cic:/DiSeL?EqTypeX/EqualityX?Mixin
IsAliasFor cic:/DiSeL?EqTypeX/EqualityX?mixin_of_C_1 cic:/DiSeL?EqTypeX/EqualityX?Mixin
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?op
constant cic:/DiSeL?EqTypeX/EqualityX?op
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?ClassDef
deriveddeclaration cic:/DiSeL?EqTypeX/EqualityX?ClassDef
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?sort
constant cic:/DiSeL?EqTypeX/EqualityX?sort
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?class
constant cic:/DiSeL?EqTypeX/EqualityX?class
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?pack
constant cic:/DiSeL?EqTypeX/EqualityX?pack
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?clone
constant cic:/DiSeL?EqTypeX/EqualityX?clone
Declares cic:/DiSeL?EqTypeX/EqualityX cic:/DiSeL?EqTypeX/EqualityX?Exports
theory cic:/DiSeL?EqTypeX/EqualityX/Exports
HasMeta cic:/DiSeL?EqTypeX/EqualityX/Exports http://coq.inria.fr/foundation?CoqSyntax
......
......@@ -19,15 +19,20 @@ dataconstructor cic:/DiSeL?Freshness?valid_fresh'
dataconstructor cic:/DiSeL?Freshness?last_fresh
theory cic:/DiSeL?Freshness
HasMeta cic:/DiSeL?Freshness http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Freshness cic:/Coq/Bool?Bool
Includes cic:/DiSeL?Freshness cic:/Coq/Classes?RelationClasses
Includes cic:/DiSeL?Freshness cic:/Coq/Classes?Morphisms_Prop
Includes cic:/DiSeL?Freshness cic:/Coq/Program?Basics
Includes cic:/DiSeL?Freshness cic:/Coq/Classes?Morphisms
Includes cic:/DiSeL?Freshness cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Freshness cic:/Coq/Init?Logic
Includes cic:/DiSeL?Freshness cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Freshness cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?Freshness cic:/fcsl/finmap?ordtype/Ordered/Exports
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?unionmap/UM
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?Freshness cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Freshness cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?Freshness cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?Freshness cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Freshness http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/DiSeL?Freshness cic:/DiSeL?Freshness?Keys
deriveddeclaration cic:/DiSeL?Freshness?Keys
......
......@@ -20,22 +20,46 @@ dataconstructor cic:/DiSeL?InferenceRules?with_inv_rule
theory cic:/DiSeL?InferenceRules
HasMeta cic:/DiSeL?InferenceRules http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Always/AlwaysInductiveInv
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?InferenceRules cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?InferenceRules cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Domain/Poset
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?InductiveInv/PWIExports
Includes cic:/DiSeL?InferenceRules cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Injection/Injection/Exports
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Actions/ActionExports
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?HoareTriples/DTbin
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Worlds/WorldGetters
Includes cic:/DiSeL?InferenceRules cic:/Coq/Init?Logic
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?InferenceRules cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?InductiveInv
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?HoareTriples
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Always
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Process
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Injection
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Actions
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Rely
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Worlds
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Protocols
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?DepMaps
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?State
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Freshness
Includes cic:/DiSeL?InferenceRules cic:/DiSeL?Domain
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?heap
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?InferenceRules cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?InferenceRules cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?InferenceRules cic:/fcsl/pcm?pred
Includes cic:/DiSeL?InferenceRules cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?InferenceRules cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?InferenceRules http://coq.inria.fr/foundation?CoqSyntax
......
theory cic:/DiSeL?Injection
HasMeta cic:/DiSeL?Injection http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Injection cic:/DiSeL?Actions
Includes cic:/DiSeL?Injection cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?Injection cic:/DiSeL?Freshness
Includes cic:/DiSeL?Injection cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?Injection cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?Injection cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Injection cic:/DiSeL?Worlds
Includes cic:/DiSeL?Injection cic:/DiSeL?Protocols
Includes cic:/DiSeL?Injection cic:/DiSeL?State
Includes cic:/DiSeL?Injection cic:/fcsl/pcm?heap
Includes cic:/DiSeL?Injection cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Injection cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Injection cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?Injection cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Injection cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?Injection cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Injection cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?Injection http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Injection cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?Injection cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?Injection cic:/DiSeL?Freshness
Includes cic:/DiSeL?Injection cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?Injection cic:/DiSeL?Actions
Declares cic:/DiSeL?Injection cic:/DiSeL?Injection?Injection
theory cic:/DiSeL?Injection/Injection
HasMeta cic:/DiSeL?Injection/Injection http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Injection/Injection cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Injection/Injection cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Injection/Injection cic:/Coq/Init?Logic
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Injection/Injection cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?State
Includes cic:/DiSeL?Injection/Injection cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Injection/Injection cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Injection/Injection cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?Worlds/WorldGetters
Declares cic:/DiSeL?Injection/Injection cic:/DiSeL?Injection/Injection?Injection
deriveddeclaration cic:/DiSeL?Injection/Injection?Injection
Declares cic:/DiSeL?Injection/Injection cic:/DiSeL?Injection/Injection?E
constant cic:/DiSeL?Injection/Injection?E
Declares cic:/DiSeL?Injection/Injection cic:/DiSeL?Injection/Injection?Exports
theory cic:/DiSeL?Injection/Injection/Exports
HasMeta cic:/DiSeL?Injection/Injection/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Injection/Injection/Exports cic:/Coq/ssr?ssrfun
Includes cic:/DiSeL?Injection/Injection/Exports cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Injection/Injection/Exports cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Injection/Injection/Exports cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Injection/Injection/Exports cic:/Coq/Init?Logic
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?pcm/CancellativePCM/Exports
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?State
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Injection/Injection/Exports cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Worlds/WorldGetters
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?Exports
deriveddeclaration cic:/DiSeL?Injection/Injection/Exports?Exports
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?inj_ext
constant cic:/DiSeL?Injection/Injection/Exports?inj_ext
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?injects
constant cic:/DiSeL?Injection/Injection/Exports?injects
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?Inject
constant cic:/DiSeL?Injection/Injection/Exports?Inject
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?cohK
constant cic:/DiSeL?Injection/Injection/Exports?cohK
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?cohE
constant cic:/DiSeL?Injection/Injection/Exports?cohE
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?sem_extend
constant cic:/DiSeL?Injection/Injection/Exports?sem_extend
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?sem_split
constant cic:/DiSeL?Injection/Injection/Exports?sem_split
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?extends
constant cic:/DiSeL?Injection/Injection/Exports?extends
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?projectS
constant cic:/DiSeL?Injection/Injection/Exports?projectS
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?projectS_cohL
constant cic:/DiSeL?Injection/Injection/Exports?projectS_cohL
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?projectS_cohR
constant cic:/DiSeL?Injection/Injection/Exports?projectS_cohR
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?projectSE
constant cic:/DiSeL?Injection/Injection/Exports?projectSE
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?coh_split
constant cic:/DiSeL?Injection/Injection/Exports?coh_split
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?injExtL'
constant cic:/DiSeL?Injection/Injection/Exports?injExtL'
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?injExtR'
constant cic:/DiSeL?Injection/Injection/Exports?injExtR'
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?injExtL
constant cic:/DiSeL?Injection/Injection/Exports?injExtL
Declares cic:/DiSeL?Injection/Injection/Exports cic:/DiSeL?Injection/Injection/Exports?injExtR
constant cic:/DiSeL?Injection/Injection/Exports?injExtR
Includes cic:/DiSeL?Injection/Injection cic:/DiSeL?Injection/Injection/Exports
Includes cic:/DiSeL?Injection cic:/DiSeL?Injection/Injection
Declares cic:/DiSeL?Injection cic:/DiSeL?Injection?InjectExtra
theory cic:/DiSeL?Injection/InjectExtra
HasMeta cic:/DiSeL?Injection/InjectExtra http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Injection/Injection
Includes cic:/DiSeL?Injection/InjectExtra cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Injection/InjectExtra cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Injection/Injection/Exports
Includes cic:/DiSeL?Injection/InjectExtra cic:/Coq/Init?Logic
Includes cic:/DiSeL?Injection/InjectExtra cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Protocols
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?pcm/CancellativePCM
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?heap/Heap
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Protocols/Transitions/Exports
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?pcm/CancellativePCM/Exports
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?pred
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Worlds/WorldGetters
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?State
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?Injection/InjectExtra cic:/fcsl/pcm?pcm/PCM
Declares cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Injection/InjectExtra?cohUnKR
constant cic:/DiSeL?Injection/InjectExtra?cohUnKR
Declares cic:/DiSeL?Injection/InjectExtra cic:/DiSeL?Injection/InjectExtra?cohUnKL
......
......@@ -13,15 +13,36 @@ dataconstructor cic:/DiSeL?NetworkSem?stepV2
dataconstructor cic:/DiSeL?NetworkSem?step_preserves_node_ids
theory cic:/DiSeL?NetworkSem
HasMeta cic:/DiSeL?NetworkSem http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?NetworkSem cic:/Coq/Init?Logic
Includes cic:/DiSeL?NetworkSem cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?NetworkSem cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?NetworkSem cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Freshness
Includes cic:/DiSeL?NetworkSem cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?NetworkSem cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols/Transitions
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?heap/Heap
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols/Transitions/Exports
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols/Coherence/Exports
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?NetworkSem cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Worlds/WorldGetters
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Worlds
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Protocols
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?State
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?heap
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?NetworkSem cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?NetworkSem cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?pred
Includes cic:/DiSeL?NetworkSem cic:/fcsl/pcm?axioms
Includes cic:/DiSeL?NetworkSem http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?NetworkSem cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?NetworkSem cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?Freshness
Includes cic:/DiSeL?NetworkSem cic:/DiSeL?EqTypeX
Declares cic:/DiSeL?NetworkSem cic:/DiSeL?NetworkSem?NetworkSemantics
deriveddeclaration cic:/DiSeL?NetworkSem?NetworkSemantics
Declares cic:/DiSeL?NetworkSem cic:/DiSeL?NetworkSem?get_coh
......
......@@ -6,13 +6,25 @@ dataconstructor cic:/DiSeL?NewStatePredicates?no_msg_spec_consume
dataconstructor cic:/DiSeL?NewStatePredicates?msg_spec_consumeE
theory cic:/DiSeL?NewStatePredicates
HasMeta cic:/DiSeL?NewStatePredicates http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/DiSeL?NewStatePredicates cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?NewStatePredicates cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?NewStatePredicates cic:/Coq/Init?Logic
Includes cic:/DiSeL?NewStatePredicates cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?NewStatePredicates cic:/DiSeL?DepMaps
Includes cic:/DiSeL?NewStatePredicates cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?NewStatePredicates cic:/DiSeL?State
Includes cic:/DiSeL?NewStatePredicates cic:/DiSeL?Freshness
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?heap
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?unionmap
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?pcm
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/finmap?finmap
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/finmap?ordtype
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?prelude
Includes cic:/DiSeL?NewStatePredicates cic:/fcsl/pcm?pred
Includes cic:/DiSeL?NewStatePredicates cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?NewStatePredicates cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?NewStatePredicates http://coq.inria.fr/foundation?CoqSyntax
......
......@@ -15,25 +15,37 @@ dataconstructor cic:/DiSeL?Process?pstep_network_sem
dataconstructor cic:/DiSeL?Process?pstep_inv
theory cic:/DiSeL?Process
HasMeta cic:/DiSeL?Process http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/DiSeL?Process cic:/DiSeL?InductiveInv/ProtocolWithInvariant
Includes cic:/DiSeL?Process cic:/Coq/Init?Datatypes
Includes cic:/DiSeL?Process cic:/Coq/ssr?ssreflect
Includes cic:/DiSeL?Process cic:/DiSeL?Actions/Actions
Includes cic:/DiSeL?Process cic:/Coq/Init?Logic
Includes cic:/DiSeL?Process cic:/DiSeL?InductiveInv/PWIExports
Includes cic:/DiSeL?Process cic:/Coq/ssr?ssrbool
Includes cic:/DiSeL?Process cic:/DiSeL?Injection/Injection/Exports
Includes cic:/DiSeL?Process cic:/DiSeL?Actions/ActionExports
Includes cic:/DiSeL?Process cic:/DiSeL?InductiveInv
Includes cic:/DiSeL?Process cic:/DiSeL?Injection
Includes cic:/DiSeL?Process cic:/DiSeL?Actions
Includes cic:/DiSeL?Process cic:/DiSeL?NetworkSem
Includes cic:/DiSeL?Process cic:/DiSeL?DepMaps
Includes cic:/DiSeL?Process cic:/DiSeL?EqTypeX
Includes cic:/DiSeL?Process cic:/DiSeL?Freshness
Includes cic:/DiSeL?Process cic:/Coq/Relations?Relation_Operators
Includes cic:/DiSeL?Process cic:/Coq/Logic?Eqdep
Includes cic:/DiSeL?Process cic:/fcsl/pcm?pcm/CancellativePCM/Exports
Includes cic:/DiSeL?Process cic:/DiSeL?Protocols/Protocols
Includes cic:/DiSeL?Process cic:/DiSeL?Protocols/Coherence
Includes cic:/DiSeL?Process cic:/fcsl/pcm?unionmap/UMC
Includes cic:/DiSeL?Process cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/DiSeL?Process cic:/fcsl/pcm?unionmap/UMDef
Includes cic:/DiSeL?Process cic:/fcsl/pcm?pcm/PCM
Includes cic:/DiSeL?Process cic:/DiSeL?State/StateGetters
Includes cic:/DiSeL?Process cic:/DiSeL?Worlds/Worlds/Core
Includes cic:/DiSeL?Process cic:/DiSeL?Protocols/Protocols/Exports
Includes cic:/DiSeL?Process cic:/DiSeL?Worlds/WorldGetters