Commit e6b42dcb authored by root's avatar root

update

parent 2c762a4a
......@@ -139,17 +139,12 @@ dataconstructor cic:/fcsl/finmap?finmap?zunit_supp
dataconstructor cic:/fcsl/finmap?finmap?zunit_disj
theory cic:/fcsl/finmap?finmap
HasMeta cic:/fcsl/finmap?finmap http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/finmap?finmap cic:/Coq/ssr?ssrfun/Option
Includes cic:/fcsl/finmap?finmap cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/finmap?finmap cic:/Coq/Classes?Morphisms_Prop
Includes cic:/fcsl/finmap?finmap cic:/Coq/Program?Basics
Includes cic:/fcsl/finmap?finmap cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/finmap?finmap cic:/Coq/Bool?Bool
Includes cic:/fcsl/finmap?finmap cic:/Coq/Init?Logic
Includes cic:/fcsl/finmap?finmap cic:/Coq/Init?Datatypes
Includes cic:/fcsl/finmap?finmap cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/finmap?finmap cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/finmap?finmap cic:/fcsl/finmap?ordtype/Ordered/Exports
Includes cic:/fcsl/finmap?finmap cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/fcsl/finmap?finmap cic:/fcsl/finmap?ordtype
Includes cic:/fcsl/finmap?finmap cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/finmap?finmap cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/finmap?finmap cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/finmap?finmap http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/fcsl/finmap?finmap cic:/fcsl/finmap?finmap?Def
deriveddeclaration cic:/fcsl/finmap?finmap?Def
......
......@@ -43,44 +43,20 @@ dataconstructor cic:/fcsl/finmap?ordtype?sorted_max_key_last
dataconstructor cic:/fcsl/finmap?ordtype?seq_last_mono
theory cic:/fcsl/finmap?ordtype
HasMeta cic:/fcsl/finmap?ordtype http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/finmap?ordtype cic:/Coq/Bool?Bool
Includes cic:/fcsl/finmap?ordtype cic:/Coq/Init?Logic
Includes cic:/fcsl/finmap?ordtype cic:/fcsl/finmap?ordtype/Ordered/Exports
Includes cic:/fcsl/finmap?ordtype cic:/Coq/Init?Datatypes
Includes cic:/fcsl/finmap?ordtype cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/finmap?ordtype cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/finmap?ordtype cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/finmap?ordtype cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/finmap?ordtype cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/finmap?ordtype http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/fcsl/finmap?ordtype cic:/fcsl/finmap?ordtype?Ordered
theory cic:/fcsl/finmap?ordtype/Ordered
HasMeta cic:/fcsl/finmap?ordtype/Ordered http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/finmap?ordtype/Ordered cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/finmap?ordtype/Ordered cic:/Coq/Init?Datatypes
Includes cic:/fcsl/finmap?ordtype/Ordered cic:/Coq/ssr?ssrbool
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?RawMixin
deriveddeclaration cic:/fcsl/finmap?ordtype/Ordered?RawMixin
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?ordering
constant cic:/fcsl/finmap?ordtype/Ordered?ordering
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?ClassDef
deriveddeclaration cic:/fcsl/finmap?ordtype/Ordered?ClassDef
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?base
constant cic:/fcsl/finmap?ordtype/Ordered?base
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?mixin
constant cic:/fcsl/finmap?ordtype/Ordered?mixin
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?sort
constant cic:/fcsl/finmap?ordtype/Ordered?sort
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?class
constant cic:/fcsl/finmap?ordtype/Ordered?class
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?clone
constant cic:/fcsl/finmap?ordtype/Ordered?clone
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?pack
constant cic:/fcsl/finmap?ordtype/Ordered?pack
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?eqType
constant cic:/fcsl/finmap?ordtype/Ordered?eqType
Declares cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered?Exports
theory cic:/fcsl/finmap?ordtype/Ordered/Exports
HasMeta cic:/fcsl/finmap?ordtype/Ordered/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/finmap?ordtype/Ordered/Exports cic:/Coq/ssr?ssrbool
Declares cic:/fcsl/finmap?ordtype/Ordered/Exports cic:/fcsl/finmap?ordtype/Ordered/Exports?ord
constant cic:/fcsl/finmap?ordtype/Ordered/Exports?ord
Includes cic:/fcsl/finmap?ordtype/Ordered cic:/fcsl/finmap?ordtype/Ordered/Exports
......
......@@ -63,10 +63,17 @@ dataconstructor cic:/fcsl/pcm?automap?undefO
dataconstructor cic:/fcsl/pcm?automap?invalidO
theory cic:/fcsl/pcm?automap
HasMeta cic:/fcsl/pcm?automap http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/fcsl/pcm?automap cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?unionmap
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?pcm
Includes cic:/fcsl/pcm?automap cic:/fcsl/finmap?ordtype
Includes cic:/fcsl/pcm?automap cic:/fcsl/pcm?pred
Includes cic:/fcsl/pcm?automap cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?automap cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap cic:/Coq/ssr?ssreflect
......@@ -208,9 +215,13 @@ constant cic:/fcsl/pcm?automap?extend_form
Declares cic:/fcsl/pcm?automap cic:/fcsl/pcm?automap?Syntactify
theory cic:/fcsl/pcm?automap/Syntactify
HasMeta cic:/fcsl/pcm?automap/Syntactify http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/Syntactify cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?automap/Syntactify cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/Syntactify cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/Syntactify cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/Syntactify cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/Syntactify cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/Syntactify cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/Syntactify cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/Syntactify cic:/fcsl/pcm?automap/Syntactify?Syntactify
deriveddeclaration cic:/fcsl/pcm?automap/Syntactify?Syntactify
......@@ -256,10 +267,15 @@ constant cic:/fcsl/pcm?automap?validO
Declares cic:/fcsl/pcm?automap cic:/fcsl/pcm?automap?ValidX
theory cic:/fcsl/pcm?automap/ValidX
HasMeta cic:/fcsl/pcm?automap/ValidX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?unionmap
Includes cic:/fcsl/pcm?automap/ValidX cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/ValidX cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?automap/Syntactify
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/ValidX cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/ValidX cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/ValidX cic:/fcsl/pcm?automap/ValidX?ValidX
deriveddeclaration cic:/fcsl/pcm?automap/ValidX?ValidX
......@@ -280,8 +296,11 @@ theory cic:/fcsl/pcm?automap/ValidX/Exports
HasMeta cic:/fcsl/pcm?automap/ValidX/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/fcsl/pcm?automap/Syntactify
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/ValidX/Exports cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/ValidX/Exports cic:/fcsl/pcm?automap/ValidX/Exports?Exports
deriveddeclaration cic:/fcsl/pcm?automap/ValidX/Exports?Exports
......@@ -296,11 +315,16 @@ constant cic:/fcsl/pcm?automap?domeqO
Declares cic:/fcsl/pcm?automap cic:/fcsl/pcm?automap?DomeqX
theory cic:/fcsl/pcm?automap/DomeqX
HasMeta cic:/fcsl/pcm?automap/DomeqX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?unionmap
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/DomeqX cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?automap/DomeqX cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?automap/Syntactify
Includes cic:/fcsl/pcm?automap/DomeqX cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/DomeqX cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?automap/DomeqX?DomeqX
deriveddeclaration cic:/fcsl/pcm?automap/DomeqX?DomeqX
......@@ -319,10 +343,13 @@ constant cic:/fcsl/pcm?automap/DomeqX?start
Declares cic:/fcsl/pcm?automap/DomeqX cic:/fcsl/pcm?automap/DomeqX?Exports
theory cic:/fcsl/pcm?automap/DomeqX/Exports
HasMeta cic:/fcsl/pcm?automap/DomeqX/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/fcsl/pcm?automap/Syntactify
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/DomeqX/Exports cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/DomeqX/Exports cic:/fcsl/pcm?automap/DomeqX/Exports?Exports
deriveddeclaration cic:/fcsl/pcm?automap/DomeqX/Exports?Exports
......@@ -341,8 +368,11 @@ theory cic:/fcsl/pcm?automap/InvalidX
HasMeta cic:/fcsl/pcm?automap/InvalidX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/InvalidX cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/pcm?automap/Syntactify
Includes cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/InvalidX cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/InvalidX cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/pcm?automap/InvalidX?InvalidX
deriveddeclaration cic:/fcsl/pcm?automap/InvalidX?InvalidX
......@@ -362,9 +392,13 @@ Declares cic:/fcsl/pcm?automap/InvalidX cic:/fcsl/pcm?automap/InvalidX?Exports
theory cic:/fcsl/pcm?automap/InvalidX/Exports
HasMeta cic:/fcsl/pcm?automap/InvalidX/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/fcsl/pcm?unionmap
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?automap/InvalidX/Exports cic:/fcsl/finmap?ordtype/Ordered
Declares cic:/fcsl/pcm?automap/InvalidX/Exports cic:/fcsl/pcm?automap/InvalidX/Exports?Exports
deriveddeclaration cic:/fcsl/pcm?automap/InvalidX/Exports?Exports
......
......@@ -23,17 +23,10 @@ dataconstructor cic:/fcsl/pcm?axioms?dyn_inj
dataconstructor cic:/fcsl/pcm?axioms?dynE
theory cic:/fcsl/pcm?axioms
HasMeta cic:/fcsl/pcm?axioms http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?axioms cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/pcm?axioms cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/pcm?axioms cic:/Coq/Logic?EqdepFacts
Includes cic:/fcsl/pcm?axioms cic:/Coq/Logic?Eqdep/EqdepTheory
Includes cic:/fcsl/pcm?axioms cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?axioms cic:/Coq/Init?Specif
Includes cic:/fcsl/pcm?axioms cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?axioms cic:/Coq/Logic?ClassicalFacts
Includes cic:/fcsl/pcm?axioms cic:/Coq/Logic?Eqdep
Includes cic:/fcsl/pcm?axioms cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?axioms cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?axioms cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?axioms cic:/Coq/Logic?Eqdep
Includes cic:/fcsl/pcm?axioms cic:/Coq/Logic?ClassicalFacts
Declares cic:/fcsl/pcm?axioms cic:/fcsl/pcm?axioms?pext
constant cic:/fcsl/pcm?axioms?pext
Declares cic:/fcsl/pcm?axioms cic:/fcsl/pcm?axioms?fext
......
This diff is collapsed.
......@@ -8,33 +8,60 @@ dataconstructor cic:/fcsl/pcm?lift?nxE0
theory cic:/fcsl/pcm?lift
HasMeta cic:/fcsl/pcm?lift http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?lift/Lift/Exports
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Logic/EqNotations
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Notations/IfNotations
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Notations
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Logic/EqNotations
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Specif
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?lift cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?lift cic:/Coq/ssrmatching?ssrmatching/SsrMatchingSyntax
Includes cic:/fcsl/pcm?lift cic:/Coq/ssrmatching?ssrmatching
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssreflect/SsrSyntax
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssreflect/TheCanonical
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssrfun/Option
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssrbool/DefaultKeying
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/CancellativePCM/Exports
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/TPCM/Exports
Includes cic:/fcsl/pcm?lift cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?lift cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/CancellativePCM
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/TPCM
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/ProdPCM
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/UnitPCM
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm/BoolConjPCM
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?pcm
Includes cic:/fcsl/pcm?lift cic:/Coq/Classes?Init
Includes cic:/fcsl/pcm?lift cic:/Coq/Program?Tactics
Includes cic:/fcsl/pcm?lift cic:/Coq/Relations?Relation_Definitions
Includes cic:/fcsl/pcm?lift cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/pcm?lift cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/fcsl/pcm?lift cic:/Coq/Classes?Morphisms_Prop
Includes cic:/fcsl/pcm?lift cic:/Coq/Program?Basics
Includes cic:/fcsl/pcm?lift cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/pcm?lift cic:/Coq/Logic?EqdepFacts/EqdepTheory
Includes cic:/fcsl/pcm?lift cic:/Coq/Logic?Eqdep/Eq_rect_eq
Includes cic:/fcsl/pcm?lift cic:/Coq/Logic?Eqdep/EqdepTheory
Includes cic:/fcsl/pcm?lift cic:/Coq/Logic?EqdepFacts
Includes cic:/fcsl/pcm?lift cic:/Coq/Logic?Eqdep
Includes cic:/fcsl/pcm?lift cic:/fcsl/pcm?prelude
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?lift cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?lift http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/fcsl/pcm?lift cic:/fcsl/pcm?lift?Unlifted
theory cic:/fcsl/pcm?lift/Unlifted
HasMeta cic:/fcsl/pcm?lift/Unlifted http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Notations/IfNotations
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Notations
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Specif
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssrmatching?ssrmatching/SsrMatchingSyntax
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssrmatching?ssrmatching
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssr?ssreflect/SsrSyntax
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssr?ssreflect/TheCanonical
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/ssr?ssrfun/Option
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Notations/IfNotations
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Notations
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Logic/EqNotations
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?lift/Unlifted cic:/Coq/Init?Datatypes
......@@ -73,8 +100,10 @@ Declares cic:/fcsl/pcm?lift/Unlifted cic:/fcsl/pcm?lift/Unlifted?Exports
theory cic:/fcsl/pcm?lift/Unlifted/Exports
HasMeta cic:/fcsl/pcm?lift/Unlifted/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/ssr?ssrfun/Option
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/Init?Notations/IfNotations
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/Init?Notations
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/Init?Logic/EqNotations
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?lift/Unlifted/Exports cic:/Coq/Init?Logic
Declares cic:/fcsl/pcm?lift/Unlifted/Exports cic:/fcsl/pcm?lift/Unlifted/Exports?ojoinC
constant cic:/fcsl/pcm?lift/Unlifted/Exports?ojoinC
......@@ -133,8 +162,11 @@ Declares cic:/fcsl/pcm?lift/Lift cic:/fcsl/pcm?lift/Lift?Exports
theory cic:/fcsl/pcm?lift/Lift/Exports
HasMeta cic:/fcsl/pcm?lift/Lift/Exports http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/fcsl/pcm?pcm/TPCM/Exports
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/fcsl/pcm?pcm/TPCM
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/fcsl/pcm?lift/Unlifted
Includes cic:/fcsl/pcm?lift/Lift/Exports cic:/Coq/Init?Logic
Declares cic:/fcsl/pcm?lift/Lift/Exports cic:/fcsl/pcm?lift/Lift/Exports?Exports
......
......@@ -28,10 +28,16 @@ dataconstructor cic:/fcsl/pcm?mutex?mx_injE
dataconstructor cic:/fcsl/pcm?mutex?mxE
theory cic:/fcsl/pcm?mutex
HasMeta cic:/fcsl/pcm?mutex http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?mutex cic:/fcsl/pcm?pcm/TPCM/Exports
Includes cic:/fcsl/pcm?mutex cic:/fcsl/pcm?pcm/TPCM
Includes cic:/fcsl/pcm?mutex cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/pcm?mutex cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/pcm?mutex cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?mutex cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?mutex cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?mutex cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?mutex cic:/fcsl/pcm?pcm
Includes cic:/fcsl/pcm?mutex cic:/fcsl/pcm?prelude
Includes cic:/fcsl/pcm?mutex cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?mutex cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?mutex cic:/Coq/ssr?ssreflect
......@@ -39,7 +45,10 @@ Includes cic:/fcsl/pcm?mutex http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/fcsl/pcm?mutex cic:/fcsl/pcm?mutex?GeneralizedMutex
theory cic:/fcsl/pcm?mutex/GeneralizedMutex
HasMeta cic:/fcsl/pcm?mutex/GeneralizedMutex http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/fcsl/pcm?pcm/TPCM
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/fcsl/pcm?pcm/CancellativePCM
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?mutex/GeneralizedMutex cic:/Coq/Init?Logic
......
......@@ -70,16 +70,29 @@ theory cic:/fcsl/pcm?natmap
HasMeta cic:/fcsl/pcm?natmap http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?natmap cic:/Coq/ssr?ssrfun/Option
Includes cic:/fcsl/pcm?natmap cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?pcm/PCM/Exports
Includes cic:/fcsl/pcm?natmap cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/pcm?natmap cic:/Coq/Classes?Morphisms_Prop
Includes cic:/fcsl/pcm?natmap cic:/Coq/Program?Basics
Includes cic:/fcsl/pcm?natmap cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/pcm?natmap cic:/fcsl/finmap?ordtype/Ordered/Exports
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap/UM
Includes cic:/fcsl/pcm?natmap cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap/UnionMapEq/Exports
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?pcm/TPCM
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap/UnionClassTPCM/Exports
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?pcm/CancellativePCM
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap/UnionMapClassCPCM/Exports
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?pcm/PCM
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap/UnionMapClassPCM/Exports
Includes cic:/fcsl/pcm?natmap cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?natmap cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap/UMC
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?unionmap
Includes cic:/fcsl/pcm?natmap cic:/fcsl/finmap?finmap
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?pcm
Includes cic:/fcsl/pcm?natmap cic:/fcsl/finmap?ordtype
Includes cic:/fcsl/pcm?natmap cic:/fcsl/pcm?prelude
Includes cic:/fcsl/pcm?natmap cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?natmap cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?natmap cic:/Coq/ssr?ssreflect
......@@ -90,6 +103,7 @@ HasMeta cic:/fcsl/pcm?natmap/NMSig http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?natmap/NMSig cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?natmap/NMSig cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/fcsl/pcm?natmap/NMSig cic:/fcsl/finmap?ordtype
Includes cic:/fcsl/pcm?natmap/NMSig cic:/fcsl/pcm?unionmap/UM
Includes cic:/fcsl/pcm?natmap/NMSig cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?natmap/NMSig cic:/Coq/Init?Datatypes
Declares cic:/fcsl/pcm?natmap/NMSig cic:/fcsl/pcm?natmap/NMSig?tp
......@@ -163,6 +177,7 @@ Includes cic:/fcsl/pcm?natmap/NMDef cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?natmap/NMDef cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?natmap/NMDef cic:/fcsl/finmap?ordtype/Ordered
Includes cic:/fcsl/pcm?natmap/NMDef cic:/fcsl/finmap?ordtype
Includes cic:/fcsl/pcm?natmap/NMDef cic:/fcsl/pcm?unionmap/UM
Includes cic:/fcsl/pcm?natmap/NMDef cic:/Coq/Init?Datatypes
Declares cic:/fcsl/pcm?natmap/NMDef cic:/fcsl/pcm?natmap/NMDef?NMDef
deriveddeclaration cic:/fcsl/pcm?natmap/NMDef?NMDef
......
This diff is collapsed.
......@@ -147,17 +147,10 @@ dataconstructor cic:/fcsl/pcm?pred?ImageIm
dataconstructor cic:/fcsl/pcm?pred?ImageEq
theory cic:/fcsl/pcm?pred
HasMeta cic:/fcsl/pcm?pred http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?pred cic:/Coq/Classes?Morphisms_Prop
Includes cic:/fcsl/pcm?pred cic:/Coq/Program?Basics
Includes cic:/fcsl/pcm?pred cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/pcm?pred cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/pcm?pred cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?pred cic:/Coq/Init?Specif
Includes cic:/fcsl/pcm?pred cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?pred cic:/Coq/Setoids?Setoid
Includes cic:/fcsl/pcm?pred cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?pred cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?pred cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?pred cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?pred cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?pred cic:/Coq/Setoids?Setoid
Includes cic:/fcsl/pcm?pred http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/fcsl/pcm?pred cic:/fcsl/pcm?pred?andTp
constant cic:/fcsl/pcm?pred?andTp
......
......@@ -51,27 +51,27 @@ dataconstructor cic:/fcsl/pcm?prelude?emptysetEqMix
dataconstructor cic:/fcsl/pcm?prelude?emptysetEqType
theory cic:/fcsl/pcm?prelude
HasMeta cic:/fcsl/pcm?prelude http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/fcsl/pcm?prelude cic:/Coq/Classes?RelationClasses
Includes cic:/fcsl/pcm?prelude cic:/Coq/Classes?Morphisms_Prop
Includes cic:/fcsl/pcm?prelude cic:/Coq/Program?Basics
Includes cic:/fcsl/pcm?prelude cic:/Coq/Classes?Morphisms
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Logic/EqNotations
Includes cic:/fcsl/pcm?prelude cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssrmatching?ssrmatching/SsrMatchingSyntax
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssrmatching?ssrmatching
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssreflect/SsrSyntax
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssreflect/TheCanonical
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Notations/IfNotations
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Notations
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Logic/EqNotations
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Specif
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Logic
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?Eqdep/Eq_rect_eq
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?Eqdep/EqdepTheory
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?Eqdep
Includes cic:/fcsl/pcm?prelude cic:/Coq/Bool?Bool
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssreflect/SsrSyntax
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssreflect/TheCanonical
Includes cic:/fcsl/pcm?prelude cic:/Coq/Init?Datatypes
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssrfun/Option
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssrbool/DefaultKeying
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssrbool
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssreflect
Includes cic:/fcsl/pcm?prelude cic:/Coq/ssr?ssrfun
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?EqdepFacts/EqdepTheory
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?EqdepFacts
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?Eqdep/Eq_rect_eq
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?Eqdep/EqdepTheory
Includes cic:/fcsl/pcm?prelude cic:/Coq/Logic?Eqdep
Includes cic:/fcsl/pcm?prelude http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/fcsl/pcm?prelude cic:/fcsl/pcm?prelude?inj_pair2
constant cic:/fcsl/pcm?prelude?inj_pair2
......
This diff is collapsed.
document https://coq.inria.fr/coq/fcsl
Declares https://coq.inria.fr/coq/fcsl https://coq.inria.fr/coq/fcsl/finmap
Declares https://coq.inria.fr/coq/fcsl https://coq.inria.fr/coq/fcsl/pcm
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment