Commit 84651be9 authored by root's avatar root

update

parent 4042f9b3
document https://coq.inria.fr/coq/ExtLib
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Core
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Data
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/ExtLib.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Generic
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Programming
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Recur
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Relations
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Structures
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Tactics
Declares https://coq.inria.fr/coq/ExtLib https://coq.inria.fr/coq/ExtLib/Tactics.theory.omdoc
......@@ -3,3 +3,36 @@ Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Da
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Char.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Checked.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Eq
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Eq.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Fin.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Fun.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Graph
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/HList.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Lazy.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/LazyList.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/List.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/ListFirstnSkipn.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/ListNth.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Map
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Member.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Monads
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/N.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Nat.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Option.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/PList.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/POption.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/PPair.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Pair.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Positive.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/PreFun.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Prop.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Set
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/SigT.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Stream.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/String.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Sum.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/SumN.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Tuple.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Unit.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Vector.theory.omdoc
Declares https://coq.inria.fr/coq/ExtLib/Data https://coq.inria.fr/coq/ExtLib/Data/Z.theory.omdoc
......@@ -15,8 +15,14 @@ dataconstructor cic:/ExtLib/Core?CmpDec?CmpDec_Correct_pair
theory cic:/ExtLib/Core?CmpDec
HasMeta cic:/ExtLib/Core?CmpDec http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Init?Logic
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Init?Notations/IfNotations
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Init?Notations
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Classes?Init
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Program?Basics
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Program?Tactics
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Core?CmpDec cic:/Coq/Bool?Bool
Includes cic:/ExtLib/Core?CmpDec http://coq.inria.fr/foundation?CoqSyntax
......
......@@ -16,18 +16,22 @@ dataconstructor cic:/ExtLib/Core?RelDec?RelDec_Correct_eq_typ
theory cic:/ExtLib/Core?RelDec
HasMeta cic:/ExtLib/Core?RelDec http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Specif
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Logic
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Notations/IfNotations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Notations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Program?Tactics
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Init
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?CMorphisms/ProperNotations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?CMorphisms
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Program?Basics
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?SetoidTactics
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Setoids?Setoid
Includes cic:/ExtLib/Core?RelDec cic:/Coq/Classes?RelationClasses
......
......@@ -29,21 +29,30 @@ dataconstructor cic:/ExtLib/Core?Type?typeOk_from_equal
dataconstructor cic:/ExtLib/Core?Type?typeOk_libniz
theory cic:/ExtLib/Core?Type
HasMeta cic:/ExtLib/Core?Type http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Logic
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Core?Type cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Notations/IfNotations
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Notations
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Init
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Core?Type cic:/Coq/Program?Basics
Includes cic:/ExtLib/Core?Type cic:/Coq/Program?Tactics
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Specif
Includes cic:/ExtLib/Core?Type cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Core?Type cic:/Coq/Relations?Relation_Operators
Includes cic:/ExtLib/Core?Type cic:/Coq/Relations?Operators_Properties
Includes cic:/ExtLib/Core?Type cic:/Coq/Relations?Relations
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?CMorphisms/ProperNotations
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?CMorphisms
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Core?Type cic:/Coq/Classes?SetoidTactics
Includes cic:/ExtLib/Core?Type cic:/ExtLib/Structures?Proper
Includes cic:/ExtLib/Core?Type cic:/Coq/Setoids?Setoid
Includes cic:/ExtLib/Core?Type http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/ExtLib/Core?Type cic:/ExtLib/Core?Type?type_DEF
deriveddeclaration cic:/ExtLib/Core?Type?type_DEF
Declares cic:/ExtLib/Core?Type cic:/ExtLib/Core?Type?type
......
......@@ -8,6 +8,7 @@ dataconstructor cic:/ExtLib/Data?Char?chr_newline
theory cic:/ExtLib/Data?Char
HasMeta cic:/ExtLib/Data?Char http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Char cic:/Coq/Init?Nat
Includes cic:/ExtLib/Data?Char cic:/ExtLib?Tactics
Includes cic:/ExtLib/Data?Char cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?Char cic:/Coq/Bool?Bool
Includes cic:/ExtLib/Data?Char cic:/Coq/Init?Datatypes
......
......@@ -11,7 +11,6 @@ dataconstructor cic:/ExtLib/Data?Eq?eq_Arr_eq
dataconstructor cic:/ExtLib/Data?Eq?eq_sym_eq_sym
theory cic:/ExtLib/Data?Eq
HasMeta cic:/ExtLib/Data?Eq http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Eq cic:/Coq/Init?Logic
Declares cic:/ExtLib/Data?Eq cic:/ExtLib/Data?Eq?eq_sym_eq
constant cic:/ExtLib/Data?Eq?eq_sym_eq
Declares cic:/ExtLib/Data?Eq cic:/ExtLib/Data?Eq?match_eq_sym_eq
......
......@@ -16,22 +16,25 @@ theory cic:/ExtLib/Data?Fin
HasMeta cic:/ExtLib/Data?Fin http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Fin cic:/Coq/Logic?Eqdep/EqdepTheory
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?EquivDec
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Specif
Includes cic:/ExtLib/Data?Fin cic:/ExtLib?Tactics
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?Fin cic:/Coq/Bool?Bool
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Notations/IfNotations
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Notations
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Data?Fin cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?Fin cic:/Coq/Init?Specif
Includes cic:/ExtLib/Data?Fin cic:/Coq/Bool?Bool
Includes cic:/ExtLib/Data?Fin cic:/Coq/Program?Tactics
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Init
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?CMorphisms/ProperNotations
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?CMorphisms
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Data?Fin cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Data?Fin cic:/Coq/Program?Basics
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?SetoidTactics
Includes cic:/ExtLib/Data?Fin cic:/Coq/Setoids?Setoid
Includes cic:/ExtLib/Data?Fin cic:/Coq/Classes?RelationClasses
......
......@@ -10,8 +10,12 @@ dataconstructor cic:/ExtLib/Data?Fun?Applicative_Fun
dataconstructor cic:/ExtLib/Data?Fun?Monoid_compose
theory cic:/ExtLib/Data?Fun
HasMeta cic:/ExtLib/Data?Fun http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Fun cic:/ExtLib/Structures?Monoid
Includes cic:/ExtLib/Data?Fun cic:/ExtLib/Structures?CoFunctor
Includes cic:/ExtLib/Data?Fun cic:/ExtLib/Structures?Applicative
Includes cic:/ExtLib/Data?Fun cic:/ExtLib/Structures?Functor
Includes cic:/ExtLib/Data?Fun cic:/ExtLib/Data?PreFun
Includes cic:/ExtLib/Data?Fun cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?Fun http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/ExtLib/Data?Fun cic:/ExtLib/Data?Fun?proper_id
constant cic:/ExtLib/Data?Fun?proper_id
Declares cic:/ExtLib/Data?Fun cic:/ExtLib/Data?Fun?functors
......
......@@ -74,12 +74,19 @@ HasMeta cic:/ExtLib/Data?HList http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?HList cic:/Coq/Arith?Minus
Includes cic:/ExtLib/Data?HList cic:/Coq/Arith?Lt
Includes cic:/ExtLib/Data?HList cic:/Coq/Init?Peano
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Data?PreFun
Includes cic:/ExtLib/Data?HList cic:/Coq/Init?Nat
Includes cic:/ExtLib/Data?HList cic:/Coq/Init?Specif
Includes cic:/ExtLib/Data?HList cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Data?HList cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?HList cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?HList cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Data?HList cic:/ExtLib?Tactics
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Data?Option
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Data?ListNth
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Data?Member
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Data?SigT
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Structures?Proper
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Core?RelDec
Includes cic:/ExtLib/Data?HList cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?HList cic:/Coq/Classes?RelationClasses
......
......@@ -7,7 +7,9 @@ dataconstructor cic:/ExtLib/Data?Lazy?Monad_Lazy
theory cic:/ExtLib/Data?Lazy
HasMeta cic:/ExtLib/Data?Lazy http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Lazy cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?Lazy http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Lazy cic:/ExtLib/Structures?Functor
Includes cic:/ExtLib/Data?Lazy cic:/ExtLib/Structures?CoMonad
Includes cic:/ExtLib/Data?Lazy cic:/ExtLib/Structures?Monad
Declares cic:/ExtLib/Data?Lazy cic:/ExtLib/Data?Lazy?Lazy
constant cic:/ExtLib/Data?Lazy?Lazy
Declares cic:/ExtLib/Data?Lazy cic:/ExtLib/Data?Lazy?_lazy
......
......@@ -9,14 +9,6 @@ dataconstructor cic:/ExtLib/Data?ListNth?nth_error_length_lt
dataconstructor cic:/ExtLib/Data?ListNth?nth_error_map
theory cic:/ExtLib/Data?ListNth
HasMeta cic:/ExtLib/Data?ListNth http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Arith?Plus
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Arith?Le
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Init?Nat
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Arith?Lt
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Init?Peano
Includes cic:/ExtLib/Data?ListNth cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?ListNth http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/ExtLib/Data?ListNth cic:/ExtLib/Data?ListNth?parametric
deriveddeclaration cic:/ExtLib/Data?ListNth?parametric
......
dataconstructor cic:/ExtLib/Data?List?type_list
dataconstructor cic:/ExtLib/Data?List?typeOk_list
dataconstructor cic:/ExtLib/Data?List?EqDec_list
dataconstructor cic:/ExtLib/Data?List?list_ind_singleton
dataconstructor cic:/ExtLib/Data?List?list_rev_ind
dataconstructor cic:/ExtLib/Data?List?allb
dataconstructor cic:/ExtLib/Data?List?anyb
dataconstructor cic:/ExtLib/Data?List?Forall_map
dataconstructor cic:/ExtLib/Data?List?Forall_cons_iff
dataconstructor cic:/ExtLib/Data?List?Forall_nil_iff
dataconstructor cic:/ExtLib/Data?List?Foldable_list
dataconstructor cic:/ExtLib/Data?List?mapT_list
dataconstructor cic:/ExtLib/Data?List?Traversable_list
dataconstructor cic:/ExtLib/Data?List?Monad_list
dataconstructor cic:/ExtLib/Data?List?wf_R_list_len_subproof
dataconstructor cic:/ExtLib/Data?List?wf_R_list_len
dataconstructor cic:/ExtLib/Data?List?Monoid_list_app
dataconstructor cic:/ExtLib/Data?List?list_eqb
dataconstructor cic:/ExtLib/Data?List?RelDec_eq_list
dataconstructor cic:/ExtLib/Data?List?RelDec_Correct_eq_list
dataconstructor cic:/ExtLib/Data?List?Injective_cons
dataconstructor cic:/ExtLib/Data?List?Injective_cons_nil
dataconstructor cic:/ExtLib/Data?List?Injective_nil_cons
......@@ -28,36 +17,28 @@ dataconstructor cic:/ExtLib/Data?List?Injective_app_same_R
dataconstructor cic:/ExtLib/Data?List?eq_list_eq
theory cic:/ExtLib/Data?List
HasMeta cic:/ExtLib/Data?List http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?List cic:/Coq/Init?Wf
Includes cic:/ExtLib/Data?List cic:/Coq/Init?Peano
Includes cic:/ExtLib/Data?List cic:/Coq/Init?Specif
Includes cic:/ExtLib/Data?List cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Data?List cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?List cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?List cic:/ExtLib/Core?RelDec
Includes cic:/ExtLib/Data?List cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?List cic:/Coq/Classes?EquivDec
Includes cic:/ExtLib/Data?List cic:/ExtLib?Tactics
Includes cic:/ExtLib/Data?List cic:/ExtLib/Structures?Applicative
Includes cic:/ExtLib/Data?List cic:/ExtLib/Structures?Monad
Includes cic:/ExtLib/Data?List cic:/ExtLib/Structures?Functor
Includes cic:/ExtLib/Data?List cic:/ExtLib/Structures?Traversable
Includes cic:/ExtLib/Data?List cic:/ExtLib/Data?Nat
Includes cic:/ExtLib/Data?List cic:/ExtLib/Structures?Reducible
Includes cic:/ExtLib/Data?List cic:/ExtLib/Structures?Monoid
Includes cic:/ExtLib/Data?List http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?List cic:/Coq/Classes?EquivDec
Includes cic:/ExtLib/Data?List cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?List cic:/ExtLib/Core?RelDec
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?type
deriveddeclaration cic:/ExtLib/Data?List?type
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?type_list
constant cic:/ExtLib/Data?List?type_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?typeOk_list
constant cic:/ExtLib/Data?List?typeOk_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?EqDec
deriveddeclaration cic:/ExtLib/Data?List?EqDec
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?EqDec_list
constant cic:/ExtLib/Data?List?EqDec_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?list_ind_singleton
constant cic:/ExtLib/Data?List?list_ind_singleton
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?list_rev_ind
constant cic:/ExtLib/Data?List?list_rev_ind
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?AllB
deriveddeclaration cic:/ExtLib/Data?List?AllB
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?allb
constant cic:/ExtLib/Data?List?allb
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?anyb
constant cic:/ExtLib/Data?List?anyb
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Forall_map
constant cic:/ExtLib/Data?List?Forall_map
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Forall_cons_iff
......@@ -68,28 +49,16 @@ Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Foldable_list
constant cic:/ExtLib/Data?List?Foldable_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?traversable
deriveddeclaration cic:/ExtLib/Data?List?traversable
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?mapT_list
constant cic:/ExtLib/Data?List?mapT_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Traversable_list
constant cic:/ExtLib/Data?List?Traversable_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Monad_list
constant cic:/ExtLib/Data?List?Monad_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?list
deriveddeclaration cic:/ExtLib/Data?List?list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?wf_R_list_len_subproof
constant cic:/ExtLib/Data?List?wf_R_list_len_subproof
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?wf_R_list_len
constant cic:/ExtLib/Data?List?wf_R_list_len
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Monoid_list_app
constant cic:/ExtLib/Data?List?Monoid_list_app
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?ListEq
deriveddeclaration cic:/ExtLib/Data?List?ListEq
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?list_eqb
constant cic:/ExtLib/Data?List?list_eqb
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?RelDec_eq_list
constant cic:/ExtLib/Data?List?RelDec_eq_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?RelDec_Correct_eq_list
constant cic:/ExtLib/Data?List?RelDec_Correct_eq_list
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Injective_cons
constant cic:/ExtLib/Data?List?Injective_cons
Declares cic:/ExtLib/Data?List cic:/ExtLib/Data?List?Injective_cons_nil
......
dataconstructor cic:/ExtLib/Data?Member?to_nat
dataconstructor cic:/ExtLib/Data?Member?member_eta
dataconstructor cic:/ExtLib/Data?Member?member_case
dataconstructor cic:/ExtLib/Data?Member?to_nat_eq_member_eq
dataconstructor cic:/ExtLib/Data?Member?nth_member
dataconstructor cic:/ExtLib/Data?Member?get_next
dataconstructor cic:/ExtLib/Data?Member?Injective_MN
dataconstructor cic:/ExtLib/Data?Member?nth_member_nth_error
dataconstructor cic:/ExtLib/Data?Member?member_In
theory cic:/ExtLib/Data?Member
HasMeta cic:/ExtLib/Data?Member http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Member cic:/Coq/Init?Specif
Includes cic:/ExtLib/Data?Member cic:/Coq/Logic?EqdepFacts
Includes cic:/ExtLib/Data?Member cic:/Coq/Classes?EquivDec
Includes cic:/ExtLib/Data?Member cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?Member cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Data?ListNth
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Core?RelDec
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?Member cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Data?Member cic:/Coq/Relations?Relations
Includes cic:/ExtLib/Data?Member cic:/ExtLib?Tactics
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Structures?Proper
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Data?Option
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Data?SigT
Includes cic:/ExtLib/Data?Member http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Member cic:/Coq/Relations?Relations
Includes cic:/ExtLib/Data?Member cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Core?RelDec
Includes cic:/ExtLib/Data?Member cic:/ExtLib/Data?ListNth
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?member
deriveddeclaration cic:/ExtLib/Data?Member?member
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?to_nat
constant cic:/ExtLib/Data?Member?to_nat
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?member_eta
constant cic:/ExtLib/Data?Member?member_eta
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?member_case
constant cic:/ExtLib/Data?Member?member_case
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?to_nat_eq_member_eq
constant cic:/ExtLib/Data?Member?to_nat_eq_member_eq
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?nth_member
constant cic:/ExtLib/Data?Member?nth_member
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?get_next
constant cic:/ExtLib/Data?Member?get_next
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?Injective_MN
constant cic:/ExtLib/Data?Member?Injective_MN
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?nth_member_nth_error
constant cic:/ExtLib/Data?Member?nth_member_nth_error
Declares cic:/ExtLib/Data?Member cic:/ExtLib/Data?Member?member_In
constant cic:/ExtLib/Data?Member?member_In
......@@ -3,11 +3,9 @@ dataconstructor cic:/ExtLib/Data?N?typeOk_N
dataconstructor cic:/ExtLib/Data?N?N_proper
theory cic:/ExtLib/Data?N
HasMeta cic:/ExtLib/Data?N http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?N cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?N cic:/Coq/Numbers?BinNums
Includes cic:/ExtLib/Data?N cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?N cic:/ExtLib/Structures?Proper
Includes cic:/ExtLib/Data?N cic:/Coq/PArith?BinPos
Includes cic:/ExtLib/Data?N http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?N cic:/ExtLib/Core?Type
Declares cic:/ExtLib/Data?N cic:/ExtLib/Data?N?type_N
constant cic:/ExtLib/Data?N?type_N
Declares cic:/ExtLib/Data?N cic:/ExtLib/Data?N?typeOk_N
......
......@@ -11,11 +11,7 @@ dataconstructor cic:/ExtLib/Data?Nat?RelDecCorrect_lt
dataconstructor cic:/ExtLib/Data?Nat?RelDecCorrect_le
dataconstructor cic:/ExtLib/Data?Nat?RelDecCorrect_gt
dataconstructor cic:/ExtLib/Data?Nat?RelDecCorrect_ge
dataconstructor cic:/ExtLib/Data?Nat?R_nat_S
dataconstructor cic:/ExtLib/Data?Nat?R_S
dataconstructor cic:/ExtLib/Data?Nat?wf_R_S
dataconstructor cic:/ExtLib/Data?Nat?R_nat_lt
dataconstructor cic:/ExtLib/Data?Nat?R_lt
dataconstructor cic:/ExtLib/Data?Nat?wf_R_lt
dataconstructor cic:/ExtLib/Data?Nat?Monoid_nat_plus
dataconstructor cic:/ExtLib/Data?Nat?Monoid_nat_mult
......@@ -24,66 +20,11 @@ dataconstructor cic:/ExtLib/Data?Nat?Injective_S
dataconstructor cic:/ExtLib/Data?Nat?nat_get_eq
theory cic:/ExtLib/Data?Nat
HasMeta cic:/ExtLib/Data?Nat http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Decimal/Little
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Decimal
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?Init
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?Morphisms_Prop
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Logic/EqNotations
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Notations/IfNotations
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Notations
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Wf
Includes cic:/ExtLib/Data?Nat cic:/Coq/Bool?Bool
Includes cic:/ExtLib/Data?Nat cic:/Coq/Logic?Decidable
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Specif
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?RelationClasses
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Nat
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?Morphisms
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?PeanoNat/Nat/Private_Parity
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/Natural/Peano?NPeano/Nat
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Peano
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZBits
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZGcd/NZGcdProp
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZGcd
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZDiv
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZLog/NZLog2UpProp
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZLog
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZAddOrder
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZMulOrder
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZSqrt
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZPow
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZParity
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/NatInt?NZAxioms
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/Natural/Abstract?NAxioms
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Even
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?PeanoNat
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/Natural/Peano?NPeano
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Logic
Includes cic:/ExtLib/Data?Nat cic:/Coq/Init?Datatypes
Includes cic:/ExtLib/Data?Nat cic:/Coq/Relations?Relation_Definitions
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?Equivalence
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?CMorphisms/ProperNotations
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?CMorphisms
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?CRelationClasses
Includes cic:/ExtLib/Data?Nat cic:/Coq/Classes?SetoidTactics
Includes cic:/ExtLib/Data?Nat cic:/Coq/Setoids?Setoid
Includes cic:/ExtLib/Data?Nat cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?Nat cic:/ExtLib/Core?RelDec
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Wf_nat
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?EqNat
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Factorial
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Compare_dec
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Peano_dec
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Between
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Mult
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Minus
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Gt
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Plus
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Lt
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Le
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Arith_base
Includes cic:/ExtLib/Data?Nat cic:/ExtLib?Tactics
Includes cic:/ExtLib/Data?Nat cic:/ExtLib/Structures?Monoid
Includes cic:/ExtLib/Data?Nat cic:/Coq/Arith?Arith
Includes cic:/ExtLib/Data?Nat cic:/ExtLib/Core?RelDec
Includes cic:/ExtLib/Data?Nat cic:/ExtLib/Core?Type
Includes cic:/ExtLib/Data?Nat http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?RelDec_eq
constant cic:/ExtLib/Data?Nat?RelDec_eq
......@@ -93,6 +34,7 @@ Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?typeOk_nat
constant cic:/ExtLib/Data?Nat?typeOk_nat
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?nat_proper
constant cic:/ExtLib/Data?Nat?nat_proper
Includes cic:/ExtLib/Data?Nat cic:/Coq/Numbers/Natural/Peano?NPeano
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?RelDec_lt
constant cic:/ExtLib/Data?Nat?RelDec_lt
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?RelDec_le
......@@ -113,20 +55,10 @@ Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?RelDecCorrect_ge
constant cic:/ExtLib/Data?Nat?RelDecCorrect_ge
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?R_nat_S_DEF
deriveddeclaration cic:/ExtLib/Data?Nat?R_nat_S_DEF
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?R_nat_S
constant cic:/ExtLib/Data?Nat?R_nat_S
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?R_S
constant cic:/ExtLib/Data?Nat?R_S
IsAliasFor cic:/ExtLib/Data?Nat?R_nat_S_C_1 cic:/ExtLib/Data?Nat?R_S
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?wf_R_S
constant cic:/ExtLib/Data?Nat?wf_R_S
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?R_nat_lt_DEF
deriveddeclaration cic:/ExtLib/Data?Nat?R_nat_lt_DEF
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?R_nat_lt
constant cic:/ExtLib/Data?Nat?R_nat_lt
Declares cic:/ExtLib/Data?Nat cic:/ExtLib/Data?Nat?R_lt
constant cic:/ExtLib/Data?Nat?R_lt
IsAliasFor cic:/ExtLib/Data?Nat?R_nat_lt_C_1 cic:/ExtLib/Data?Nat?R_lt