Commit 0e225a44 authored by root's avatar root

update

parent 6b04adbd
This diff is collapsed.
......@@ -2,7 +2,6 @@ dataconstructor cic:/Equations?Classes?WellFounded
dataconstructor cic:/Equations?Classes?wellfounded
theory cic:/Equations?Classes
HasMeta cic:/Equations?Classes http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Classes cic:/Coq/Init?Wf
Includes cic:/Equations?Classes cic:/Coq/Relations?Relation_Definitions
Declares cic:/Equations?Classes cic:/Equations?Classes?WellFounded
constant cic:/Equations?Classes?WellFounded
......
......@@ -3,4 +3,6 @@ HasMeta cic:/Equations?ConstantsType http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?ConstantsType cic:/Coq/Relations?Relations
Includes cic:/Equations?ConstantsType cic:/Coq/Classes?CRelationClasses
Includes cic:/Equations?ConstantsType cic:/Equations?Classes
Includes cic:/Equations?ConstantsType http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?ConstantsType cic:/Equations?FunctionalInduction
Includes cic:/Equations?ConstantsType cic:/Equations?DepElim
Includes cic:/Equations?ConstantsType cic:/Equations?Init
......@@ -3,10 +3,12 @@ dataconstructor cic:/Equations?Constants?eq_sig_pack
dataconstructor cic:/Equations?Constants?eq_Signature
theory cic:/Equations?Constants
HasMeta cic:/Equations?Constants http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Constants cic:/Coq/Init?Logic
Includes cic:/Equations?Constants cic:/Coq/Relations?Relations
Includes cic:/Equations?Constants cic:/Equations?Signature
Includes cic:/Equations?Constants cic:/Equations?FunctionalInduction
Includes cic:/Equations?Constants cic:/Equations?DepElim
Includes cic:/Equations?Constants cic:/Equations?Init
Includes cic:/Equations?Constants cic:/Equations?Classes
Includes cic:/Equations?Constants http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Constants cic:/Coq/Relations?Relations
Declares cic:/Equations?Constants cic:/Equations?Constants?eq_sig
constant cic:/Equations?Constants?eq_sig
Declares cic:/Equations?Constants cic:/Equations?Constants?eq_sig_pack
......
theory cic:/Equations?DepElimDec
HasMeta cic:/Equations?DepElimDec http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?DepElimDec cic:/Equations?HSetInstances
Includes cic:/Equations?DepElimDec cic:/Equations?EqDec
Includes cic:/Equations?DepElimDec cic:/Equations?DepElim
Includes cic:/Equations?DepElimDec http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?DepElimDec cic:/Equations?Signature
Includes cic:/Equations?DepElimDec cic:/Equations?Init
dataconstructor cic:/Equations?DepElim?block
dataconstructor cic:/Equations?DepElim?NoConfusionPackage
dataconstructor cic:/Equations?DepElim?Build_NoConfusionPackage
dataconstructor cic:/Equations?DepElim?NoConfusion
dataconstructor cic:/Equations?DepElim?noConfusion
dataconstructor cic:/Equations?DepElim?noConfusion_inv
dataconstructor cic:/Equations?DepElim?noConfusion_is_equiv
dataconstructor cic:/Equations?DepElim?NoConfusionIdPackage
dataconstructor cic:/Equations?DepElim?Build_NoConfusionIdPackage
dataconstructor cic:/Equations?DepElim?NoConfusionId
dataconstructor cic:/Equations?DepElim?noConfusionId
dataconstructor cic:/Equations?DepElim?noConfusionId_inv
......@@ -16,8 +12,6 @@ dataconstructor cic:/Equations?DepElim?internal_Id_rew
dataconstructor cic:/Equations?DepElim?apply_noConfusionId
dataconstructor cic:/Equations?DepElim?False_rect_dep
dataconstructor cic:/Equations?DepElim?True_rect_dep
dataconstructor cic:/Equations?DepElim?DependentEliminationPackage
dataconstructor cic:/Equations?DepElim?Build_DependentEliminationPackage
dataconstructor cic:/Equations?DepElim?elim_type
dataconstructor cic:/Equations?DepElim?elim
dataconstructor cic:/Equations?DepElim?solution_left
......@@ -82,30 +76,20 @@ dataconstructor cic:/Equations?DepElim?Id_simplify_ind_pack_inv
dataconstructor cic:/Equations?DepElim?inaccessible_pattern
dataconstructor cic:/Equations?DepElim?hide_pattern
dataconstructor cic:/Equations?DepElim?add_pattern
dataconstructor cic:/Equations?DepElim?end_of_section
dataconstructor cic:/Equations?DepElim?the_end_of_the_section
dataconstructor cic:/Equations?DepElim?ImpossibleCall
dataconstructor cic:/Equations?DepElim?is_impossible_call
dataconstructor cic:/Equations?DepElim?elim_impossible_call
theory cic:/Equations?DepElim
HasMeta cic:/Equations?DepElim http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?DepElim cic:/Coq/Init?Notations/IfNotations
Includes cic:/Equations?DepElim cic:/Coq/Init?Notations
Includes cic:/Equations?DepElim cic:/Coq/Init?Specif
Includes cic:/Equations?DepElim cic:/Coq/Init?Logic/EqNotations
Includes cic:/Equations?DepElim cic:/Coq/Init?Logic
Includes cic:/Equations?DepElim cic:/Coq/Init?Datatypes
Includes cic:/Equations?DepElim cic:/Equations?HSets
Includes cic:/Equations?DepElim cic:/Equations?EqDec
Includes cic:/Equations?DepElim cic:/Equations?Signature
Includes cic:/Equations?DepElim cic:/Equations?Init
Includes cic:/Equations?DepElim cic:/Coq/Program?Tactics
Includes cic:/Equations?DepElim http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Equations?DepElim cic:/Equations?DepElim?block
constant cic:/Equations?DepElim?block
Declares cic:/Equations?DepElim cic:/Equations?DepElim?NoConfusionPackage_DEF
deriveddeclaration cic:/Equations?DepElim?NoConfusionPackage_DEF
Declares cic:/Equations?DepElim cic:/Equations?DepElim?NoConfusionPackage
constant cic:/Equations?DepElim?NoConfusionPackage
Declares cic:/Equations?DepElim cic:/Equations?DepElim?Build_NoConfusionPackage
constant cic:/Equations?DepElim?Build_NoConfusionPackage
IsAliasFor cic:/Equations?DepElim?NoConfusionPackage_C_1 cic:/Equations?DepElim?Build_NoConfusionPackage
Declares cic:/Equations?DepElim cic:/Equations?DepElim?NoConfusion
constant cic:/Equations?DepElim?NoConfusion
Declares cic:/Equations?DepElim cic:/Equations?DepElim?noConfusion
......@@ -116,11 +100,6 @@ Declares cic:/Equations?DepElim cic:/Equations?DepElim?noConfusion_is_equiv
constant cic:/Equations?DepElim?noConfusion_is_equiv
Declares cic:/Equations?DepElim cic:/Equations?DepElim?NoConfusionIdPackage_DEF
deriveddeclaration cic:/Equations?DepElim?NoConfusionIdPackage_DEF
Declares cic:/Equations?DepElim cic:/Equations?DepElim?NoConfusionIdPackage
constant cic:/Equations?DepElim?NoConfusionIdPackage
Declares cic:/Equations?DepElim cic:/Equations?DepElim?Build_NoConfusionIdPackage
constant cic:/Equations?DepElim?Build_NoConfusionIdPackage
IsAliasFor cic:/Equations?DepElim?NoConfusionIdPackage_C_1 cic:/Equations?DepElim?Build_NoConfusionIdPackage
Declares cic:/Equations?DepElim cic:/Equations?DepElim?NoConfusionId
constant cic:/Equations?DepElim?NoConfusionId
Declares cic:/Equations?DepElim cic:/Equations?DepElim?noConfusionId
......@@ -141,11 +120,6 @@ Declares cic:/Equations?DepElim cic:/Equations?DepElim?True_rect_dep
constant cic:/Equations?DepElim?True_rect_dep
Declares cic:/Equations?DepElim cic:/Equations?DepElim?DependentEliminationPackage_DEF
deriveddeclaration cic:/Equations?DepElim?DependentEliminationPackage_DEF
Declares cic:/Equations?DepElim cic:/Equations?DepElim?DependentEliminationPackage
constant cic:/Equations?DepElim?DependentEliminationPackage
Declares cic:/Equations?DepElim cic:/Equations?DepElim?Build_DependentEliminationPackage
constant cic:/Equations?DepElim?Build_DependentEliminationPackage
IsAliasFor cic:/Equations?DepElim?DependentEliminationPackage_C_1 cic:/Equations?DepElim?Build_DependentEliminationPackage
Declares cic:/Equations?DepElim cic:/Equations?DepElim?elim_type
constant cic:/Equations?DepElim?elim_type
Declares cic:/Equations?DepElim cic:/Equations?DepElim?elim
......@@ -280,10 +254,6 @@ Declares cic:/Equations?DepElim cic:/Equations?DepElim?add_pattern
constant cic:/Equations?DepElim?add_pattern
Declares cic:/Equations?DepElim cic:/Equations?DepElim?end_of_section_DEF
deriveddeclaration cic:/Equations?DepElim?end_of_section_DEF
Declares cic:/Equations?DepElim cic:/Equations?DepElim?end_of_section
constant cic:/Equations?DepElim?end_of_section
Declares cic:/Equations?DepElim cic:/Equations?DepElim?the_end_of_the_section
constant cic:/Equations?DepElim?the_end_of_the_section
Declares cic:/Equations?DepElim cic:/Equations?DepElim?ImpossibleCall
constant cic:/Equations?DepElim?ImpossibleCall
Declares cic:/Equations?DepElim cic:/Equations?DepElim?is_impossible_call
......
......@@ -8,12 +8,13 @@ dataconstructor cic:/Equations?EqDecInstances?sigma_eqdec
dataconstructor cic:/Equations?EqDecInstances?eqdec_sig
theory cic:/Equations?EqDecInstances
HasMeta cic:/Equations?EqDecInstances http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?EqDecInstances cic:/Equations?Init
Includes cic:/Equations?EqDecInstances cic:/Coq/Init?Logic
Includes cic:/Equations?EqDecInstances cic:/Coq/Init?Specif
Includes cic:/Equations?EqDecInstances cic:/Coq/Init?Datatypes
Includes cic:/Equations?EqDecInstances cic:/Equations?NoConfusion
Includes cic:/Equations?EqDecInstances cic:/Equations?DepElim
Includes cic:/Equations?EqDecInstances cic:/Equations?EqDec
Includes cic:/Equations?EqDecInstances http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Equations?EqDecInstances cic:/Equations?EqDecInstances?unit_eqdec
constant cic:/Equations?EqDecInstances?unit_eqdec
Declares cic:/Equations?EqDecInstances cic:/Equations?EqDecInstances?bool_eqdec
......
......@@ -28,9 +28,7 @@ dataconstructor cic:/Equations?EqDec?inj_right_sigma_refl
dataconstructor cic:/Equations?EqDec?eq_eqdec
theory cic:/Equations?EqDec
HasMeta cic:/Equations?EqDec http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?EqDec cic:/Coq/Init?Logic
Includes cic:/Equations?EqDec cic:/Coq/Init?Specif
Includes cic:/Equations?EqDec http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?EqDec cic:/Equations?Init
Declares cic:/Equations?EqDec cic:/Equations?EqDec?dec_eq
constant cic:/Equations?EqDec?dec_eq
Declares cic:/Equations?EqDec cic:/Equations?EqDec?EqDec
......
theory cic:/Equations?Equations
HasMeta cic:/Equations?Equations http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Equations http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Equations cic:/Equations?Telescopes
Includes cic:/Equations?Equations cic:/Equations?Loader
This diff is collapsed.
......@@ -9,14 +9,23 @@ theory cic:/Equations?FunctionalInduction
HasMeta cic:/Equations?FunctionalInduction http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?FunctionalInduction cic:/Coq/Init?Notations/IfNotations
Includes cic:/Equations?FunctionalInduction cic:/Coq/Init?Notations
Includes cic:/Equations?FunctionalInduction cic:/Coq/Init?Specif
Includes cic:/Equations?FunctionalInduction cic:/Coq/Init?Logic/EqNotations
Includes cic:/Equations?FunctionalInduction cic:/Coq/Init?Logic
Includes cic:/Equations?FunctionalInduction cic:/Coq/Init?Datatypes
Includes cic:/Equations?FunctionalInduction cic:/Coq/Bool?Sumbool
Includes cic:/Equations?FunctionalInduction cic:/Coq/Program?Utils
Includes cic:/Equations?FunctionalInduction cic:/Coq/Program?Tactics
Includes cic:/Equations?FunctionalInduction cic:/Coq/Program?Basics
Includes cic:/Equations?FunctionalInduction cic:/Coq/extraction?Extraction
Includes cic:/Equations?FunctionalInduction cic:/Coq/Unicode?Utf8_core
Includes cic:/Equations?FunctionalInduction cic:/Equations?Init/Sigma_Notations
Includes cic:/Equations?FunctionalInduction cic:/Equations?Init/Id_Notations
Includes cic:/Equations?FunctionalInduction cic:/Equations?Init
Includes cic:/Equations?FunctionalInduction cic:/Equations?EqDec
Includes cic:/Equations?FunctionalInduction cic:/Equations?HSets
Includes cic:/Equations?FunctionalInduction cic:/Equations?Signature
Includes cic:/Equations?FunctionalInduction cic:/Equations?DepElim/Inaccessible_Notations
Includes cic:/Equations?FunctionalInduction cic:/Equations?DepElim
Includes cic:/Equations?FunctionalInduction cic:/Equations?EqDec
Declares cic:/Equations?FunctionalInduction cic:/Equations?FunctionalInduction?FunctionalInduction_DEF
deriveddeclaration cic:/Equations?FunctionalInduction?FunctionalInduction_DEF
Declares cic:/Equations?FunctionalInduction cic:/Equations?FunctionalInduction?FunctionalInduction
......
......@@ -8,10 +8,9 @@ dataconstructor cic:/Equations?HSetInstances?list_eqdec
dataconstructor cic:/Equations?HSetInstances?eqdec_sig_Id
theory cic:/Equations?HSetInstances
HasMeta cic:/Equations?HSetInstances http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?HSetInstances cic:/Coq/Init?Logic
Includes cic:/Equations?HSetInstances cic:/Coq/Init?Datatypes
Includes cic:/Equations?HSetInstances cic:/Equations?HSets
Includes cic:/Equations?HSetInstances cic:/Equations?Init
Includes cic:/Equations?HSetInstances cic:/Equations?DepElim
Includes cic:/Equations?HSetInstances http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Equations?HSetInstances cic:/Equations?HSetInstances?eqdec_hset
constant cic:/Equations?HSetInstances?eqdec_hset
Declares cic:/Equations?HSetInstances cic:/Equations?HSetInstances?unit_eqdec
......
......@@ -31,7 +31,20 @@ dataconstructor cic:/Equations?HSets?inj_sigma_r_refl
dataconstructor cic:/Equations?HSets?K
theory cic:/Equations?HSets
HasMeta cic:/Equations?HSets http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?HSets http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?HSets cic:/Coq/Init?Notations/IfNotations
Includes cic:/Equations?HSets cic:/Coq/Init?Notations
Includes cic:/Equations?HSets cic:/Coq/Init?Logic/EqNotations
Includes cic:/Equations?HSets cic:/Coq/Init?Logic
Includes cic:/Equations?HSets cic:/Coq/Init?Datatypes
Includes cic:/Equations?HSets cic:/Coq/Bool?Sumbool
Includes cic:/Equations?HSets cic:/Coq/Program?Utils
Includes cic:/Equations?HSets cic:/Coq/Program?Tactics
Includes cic:/Equations?HSets cic:/Coq/Program?Basics
Includes cic:/Equations?HSets cic:/Coq/extraction?Extraction
Includes cic:/Equations?HSets cic:/Coq/Unicode?Utf8_core
Includes cic:/Equations?HSets cic:/Equations?Init/Sigma_Notations
Includes cic:/Equations?HSets cic:/Equations?Init/Id_Notations
Includes cic:/Equations?HSets cic:/Equations?Init
Declares cic:/Equations?HSets cic:/Equations?HSets?HProp
constant cic:/Equations?HSets?HProp
Declares cic:/Equations?HSets cic:/Equations?HSets?is_hprop
......
......@@ -3,20 +3,15 @@ dataconstructor cic:/Equations?Init?hidebody
dataconstructor cic:/Equations?Init?pr1
dataconstructor cic:/Equations?Init?pr2
dataconstructor cic:/Equations?Init?prod
dataconstructor cic:/Equations?Init?Empty
dataconstructor cic:/Equations?Init?Id
dataconstructor cic:/Equations?Init?id_refl
dataconstructor cic:/Equations?Init?id_sym
dataconstructor cic:/Equations?Init?id_trans
theory cic:/Equations?Init
HasMeta cic:/Equations?Init http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Init cic:/Coq/Init?Datatypes
Includes cic:/Equations?Init cic:/Coq/Bool?Sumbool
Includes cic:/Equations?Init cic:/Coq/Program?Utils
Includes cic:/Equations?Init cic:/Coq/Program?Tactics
Includes cic:/Equations?Init cic:/Coq/Program?Basics
Includes cic:/Equations?Init cic:/Coq/extraction?Extraction
Includes cic:/Equations?Init cic:/Coq/Unicode?Utf8_core
Includes cic:/Equations?Init cic:/Coq/extraction?Extraction
Includes cic:/Equations?Init cic:/Coq/Program?Basics
Includes cic:/Equations?Init cic:/Coq/Program?Tactics
Includes cic:/Equations?Init cic:/Coq/Program?Utils
Declares cic:/Equations?Init cic:/Equations?Init?fixproto
constant cic:/Equations?Init?fixproto
Declares cic:/Equations?Init cic:/Equations?Init?hidebody
......@@ -33,15 +28,8 @@ HasMeta cic:/Equations?Init/Sigma_Notations http://coq.inria.fr/foundation?CoqSy
Includes cic:/Equations?Init cic:/Equations?Init/Sigma_Notations
Declares cic:/Equations?Init cic:/Equations?Init?Empty_DEF
deriveddeclaration cic:/Equations?Init?Empty_DEF
Declares cic:/Equations?Init cic:/Equations?Init?Empty
constant cic:/Equations?Init?Empty
Declares cic:/Equations?Init cic:/Equations?Init?Id_DEF
deriveddeclaration cic:/Equations?Init?Id_DEF
Declares cic:/Equations?Init cic:/Equations?Init?Id
constant cic:/Equations?Init?Id
Declares cic:/Equations?Init cic:/Equations?Init?id_refl
constant cic:/Equations?Init?id_refl
IsAliasFor cic:/Equations?Init?Id_C_1 cic:/Equations?Init?id_refl
Declares cic:/Equations?Init cic:/Equations?Init?Id_Notations
theory cic:/Equations?Init/Id_Notations
HasMeta cic:/Equations?Init/Id_Notations http://coq.inria.fr/foundation?CoqSyntax
......
theory cic:/Equations?Loader
HasMeta cic:/Equations?Loader http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Loader cic:/Coq/Logic?ProofIrrelevance
Includes cic:/Equations?Loader cic:/Coq/Logic?FunctionalExtensionality
Includes cic:/Equations?Loader cic:/Coq/Program?Wf
Includes cic:/Equations?Loader cic:/Coq/Program?Utils
Includes cic:/Equations?Loader cic:/Equations?DepElimDec
Includes cic:/Equations?Loader cic:/Equations?Init
Includes cic:/Equations?Loader cic:/Equations?HSetInstances
Includes cic:/Equations?Loader cic:/Equations?EqDecInstances
Includes cic:/Equations?Loader cic:/Equations?Constants
Includes cic:/Equations?Loader cic:/Equations?Below
Includes cic:/Equations?Loader cic:/Equations?FunctionalInduction
Includes cic:/Equations?Loader cic:/Equations?DepElim
Includes cic:/Equations?Loader cic:/Equations?Classes
Includes cic:/Equations?Loader cic:/Equations?Subterm
Includes cic:/Equations?Loader cic:/Equations?NoConfusion
Includes cic:/Equations?Loader cic:/Equations?Signature
Includes cic:/Equations?Loader cic:/Coq/extraction?Extraction
Includes cic:/Equations?Loader http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Loader cic:/Equations?Classes
Includes cic:/Equations?Loader cic:/Equations?DepElim
Includes cic:/Equations?Loader cic:/Equations?FunctionalInduction
Includes cic:/Equations?Loader cic:/Equations?Below
Includes cic:/Equations?Loader cic:/Equations?Constants
Includes cic:/Equations?Loader cic:/Equations?EqDecInstances
Includes cic:/Equations?Loader cic:/Equations?HSetInstances
Includes cic:/Equations?Loader cic:/Equations?Init
Includes cic:/Equations?Loader cic:/Equations?DepElimDec
Includes cic:/Equations?Loader cic:/Coq/Program?Utils
Includes cic:/Equations?Loader cic:/Coq/Program?Wf
Includes cic:/Equations?Loader cic:/Coq/Logic?FunctionalExtensionality
Includes cic:/Equations?Loader cic:/Coq/Logic?ProofIrrelevance
......@@ -45,16 +45,13 @@ dataconstructor cic:/Equations?NoConfusion?noConfusion_sig_obligation_3
dataconstructor cic:/Equations?NoConfusion?NoConfusionPackage_sig
theory cic:/Equations?NoConfusion
HasMeta cic:/Equations?NoConfusion http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?NoConfusion cic:/Coq/Init?Specif
Includes cic:/Equations?NoConfusion cic:/Equations?Init
Includes cic:/Equations?NoConfusion cic:/Coq/Init?Logic
Includes cic:/Equations?NoConfusion cic:/Coq/Init?Datatypes
Includes cic:/Equations?NoConfusion cic:/Equations?DepElim
Includes cic:/Equations?NoConfusion cic:/Equations?Constants
Includes cic:/Equations?NoConfusion cic:/Equations?EqDec
Includes cic:/Equations?NoConfusion cic:/Coq/Bool?Bvector
Includes cic:/Equations?NoConfusion cic:/Equations?Signature
Includes cic:/Equations?NoConfusion cic:/Coq/Program?Tactics
Includes cic:/Equations?NoConfusion cic:/Coq/Bool?Bvector
Includes cic:/Equations?NoConfusion http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?NoConfusion cic:/Equations?EqDec
Includes cic:/Equations?NoConfusion cic:/Equations?Constants
Includes cic:/Equations?NoConfusion cic:/Equations?DepElim
Declares cic:/Equations?NoConfusion cic:/Equations?NoConfusion?NoConfusion_unit
constant cic:/Equations?NoConfusion?NoConfusion_unit
Declares cic:/Equations?NoConfusion cic:/Equations?NoConfusion?noConfusion_unit_obligation_1
......
......@@ -4,22 +4,21 @@ dataconstructor cic:/Equations?Signature?signature
dataconstructor cic:/Equations?Signature?signature_pack
theory cic:/Equations?Signature
HasMeta cic:/Equations?Signature http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Signature cic:/Coq/Init?Logic/EqNotations
Includes cic:/Equations?Signature cic:/Coq/Init?Logic
Includes cic:/Equations?Signature cic:/Coq/Init?Datatypes
Includes cic:/Equations?Signature cic:/Coq/Init?Notations/IfNotations
Includes cic:/Equations?Signature cic:/Coq/Init?Notations
Includes cic:/Equations?Signature cic:/Coq/Init?Specif
Includes cic:/Equations?Signature cic:/Equations?EqDec
Includes cic:/Equations?Signature cic:/Coq/Bool?Sumbool
Includes cic:/Equations?Signature cic:/Coq/Program?Utils
Includes cic:/Equations?Signature cic:/Coq/Program?Tactics
Includes cic:/Equations?Signature cic:/Coq/Program?Basics
Includes cic:/Equations?Signature cic:/Coq/extraction?Extraction
Includes cic:/Equations?Signature cic:/Coq/Unicode?Utf8_core
Includes cic:/Equations?Signature cic:/Coq/extraction?Extraction
Includes cic:/Equations?Signature cic:/Coq/Program?Basics
Includes cic:/Equations?Signature cic:/Coq/Program?Tactics
Includes cic:/Equations?Signature cic:/Coq/Program?Utils
Includes cic:/Equations?Signature cic:/Equations?Init/Sigma_Notations
Includes cic:/Equations?Signature cic:/Equations?Init/Id_Notations
Includes cic:/Equations?Signature cic:/Equations?Init
Includes cic:/Equations?Signature cic:/Coq/Init?Notations/IfNotations
Includes cic:/Equations?Signature cic:/Coq/Init?Notations
Includes cic:/Equations?Signature cic:/Coq/Init?Logic/EqNotations
Includes cic:/Equations?Signature cic:/Coq/Init?Logic
Includes cic:/Equations?Signature cic:/Coq/Init?Datatypes
Includes cic:/Equations?Signature cic:/Coq/Bool?Sumbool
Includes cic:/Equations?Signature cic:/Equations?EqDec
Declares cic:/Equations?Signature cic:/Equations?Signature?Signature_DEF
deriveddeclaration cic:/Equations?Signature?Signature_DEF
Declares cic:/Equations?Signature cic:/Equations?Signature?Signature
......
......@@ -6,34 +6,22 @@ dataconstructor cic:/Equations?Subterm?WellFounded_trans_clos
dataconstructor cic:/Equations?Subterm?wf_MR
dataconstructor cic:/Equations?Subterm?lt_wf
dataconstructor cic:/Equations?Subterm?clos_trans_stepr
dataconstructor cic:/Equations?Subterm?acc_A_B_lexprod
dataconstructor cic:/Equations?Subterm?wf_lexprod
dataconstructor cic:/Equations?Subterm?wellfounded_lexprod
theory cic:/Equations?Subterm
HasMeta cic:/Equations?Subterm http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Equations?Subterm cic:/Equations?DepElim
Includes cic:/Equations?Subterm cic:/Coq/Wellfounded?Lexicographic_Product
Includes cic:/Equations?Subterm cic:/Coq/Wellfounded?Wellfounded
Includes cic:/Equations?Subterm cic:/Coq/Init?Peano
Includes cic:/Equations?Subterm cic:/Coq/Init?Datatypes
Includes cic:/Equations?Subterm cic:/Coq/Relations?Relation_Operators
Includes cic:/Equations?Subterm cic:/Coq/Wellfounded?Transitive_Closure
Includes cic:/Equations?Subterm cic:/Coq/Init?Logic
Includes cic:/Equations?Subterm cic:/Coq/Init?Wf
Includes cic:/Equations?Subterm cic:/Coq/Relations?Relation_Definitions
Includes cic:/Equations?Subterm cic:/Equations?NoConfusion
Includes cic:/Equations?Subterm cic:/Equations?EqDec
Includes cic:/Equations?Subterm cic:/Equations?Signature
Includes cic:/Equations?Subterm cic:/Equations?Below
Includes cic:/Equations?Subterm cic:/Equations?Classes
Includes cic:/Equations?Subterm cic:/Equations?Init
Includes cic:/Equations?Subterm cic:/Coq/Logic?ProofIrrelevance
Includes cic:/Equations?Subterm cic:/Coq/Logic?FunctionalExtensionality
Includes cic:/Equations?Subterm cic:/Coq/Program?Wf
Includes cic:/Equations?Subterm cic:/Coq/Relations?Relations
Includes cic:/Equations?Subterm cic:/Coq/Bool?Bvector
Includes cic:/Equations?Subterm cic:/Coq/Arith?Lt
Includes cic:/Equations?Subterm cic:/Coq/Arith?Wf_nat
Includes cic:/Equations?Subterm cic:/Coq/Arith?Lt
Includes cic:/Equations?Subterm cic:/Coq/Bool?Bvector
Includes cic:/Equations?Subterm cic:/Coq/Relations?Relations
Includes cic:/Equations?Subterm cic:/Coq/Program?Wf
Includes cic:/Equations?Subterm cic:/Coq/Logic?FunctionalExtensionality
Includes cic:/Equations?Subterm cic:/Coq/Logic?ProofIrrelevance
Includes cic:/Equations?Subterm cic:/Equations?Init
Includes cic:/Equations?Subterm cic:/Equations?Classes
Includes cic:/Equations?Subterm cic:/Equations?Below
Includes cic:/Equations?Subterm cic:/Equations?Signature
Includes cic:/Equations?Subterm cic:/Equations?EqDec
Includes cic:/Equations?Subterm cic:/Equations?NoConfusion
Declares cic:/Equations?Subterm cic:/Equations?Subterm?FixWf
constant cic:/Equations?Subterm?FixWf
Declares cic:/Equations?Subterm cic:/Equations?Subterm?Acc_pi
......@@ -42,6 +30,7 @@ Declares cic:/Equations?Subterm cic:/Equations?Subterm?FixWf_unfold
constant cic:/Equations?Subterm?FixWf_unfold
Declares cic:/Equations?Subterm cic:/Equations?Subterm?FixWf_unfold_step
constant cic:/Equations?Subterm?FixWf_unfold_step
Includes cic:/Equations?Subterm cic:/Coq/Wellfounded?Transitive_Closure
Declares cic:/Equations?Subterm cic:/Equations?Subterm?WellFounded_trans_clos
constant cic:/Equations?Subterm?WellFounded_trans_clos
Declares cic:/Equations?Subterm cic:/Equations?Subterm?wf_MR
......@@ -50,11 +39,11 @@ Declares cic:/Equations?Subterm cic:/Equations?Subterm?lt_wf
constant cic:/Equations?Subterm?lt_wf
Declares cic:/Equations?Subterm cic:/Equations?Subterm?clos_trans_stepr
constant cic:/Equations?Subterm?clos_trans_stepr
Includes cic:/Equations?Subterm cic:/Coq/Wellfounded?Wellfounded
Includes cic:/Equations?Subterm cic:/Coq/Relations?Relation_Definitions
Includes cic:/Equations?Subterm cic:/Coq/Relations?Relation_Operators
Includes cic:/Equations?Subterm cic:/Coq/Wellfounded?Lexicographic_Product
Declares cic:/Equations?Subterm cic:/Equations?Subterm?Lexicographic_Product
deriveddeclaration cic:/Equations?Subterm?Lexicographic_Product
Declares cic:/Equations?Subterm cic:/Equations?Subterm?acc_A_B_lexprod
constant cic:/Equations?Subterm?acc_A_B_lexprod
Declares cic:/Equations?Subterm cic:/Equations?Subterm?wf_lexprod
constant cic:/Equations?Subterm?wf_lexprod
Declares cic:/Equations?Subterm cic:/Equations?Subterm?wellfounded_lexprod
constant cic:/Equations?Subterm?wellfounded_lexprod
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