Commit 985aaf91 authored by root's avatar root

update

parent 52a2c35b
dataconstructor cic:/Coquelicot?Compactness?completeness_any
dataconstructor cic:/Coquelicot?Compactness?false_not_not
dataconstructor cic:/Coquelicot?Compactness?Tn
dataconstructor cic:/Coquelicot?Compactness?bounded_n
dataconstructor cic:/Coquelicot?Compactness?close_n
dataconstructor cic:/Coquelicot?Compactness?compactness_list
dataconstructor cic:/Coquelicot?Compactness?compactness_value
dataconstructor cic:/Coquelicot?Compactness?compactness_value_1d
dataconstructor cic:/Coquelicot?Compactness?compactness_value_2d
theory cic:/Coquelicot?Compactness
HasMeta cic:/Coquelicot?Compactness http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Compactness cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?Compactness cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?Compactness cic:/Coq/Reals?DiscrR
Includes cic:/Coquelicot?Compactness cic:/Coq/micromega?Fourier_util
Includes cic:/Coquelicot?Compactness cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Compactness cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Compactness cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Compactness cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?Compactness cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Compactness cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Compactness cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Compactness cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Compactness cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Compactness cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Compactness http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?completeness_any
......@@ -12,6 +30,16 @@ Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?false_not_not
constant cic:/Coquelicot?Compactness?false_not_not
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?Compactness
deriveddeclaration cic:/Coquelicot?Compactness?Compactness
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?Tn
constant cic:/Coquelicot?Compactness?Tn
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?bounded_n
constant cic:/Coquelicot?Compactness?bounded_n
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?close_n
constant cic:/Coquelicot?Compactness?close_n
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?compactness_list
constant cic:/Coquelicot?Compactness?compactness_list
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?compactness_value
constant cic:/Coquelicot?Compactness?compactness_value
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?compactness_value_1d
constant cic:/Coquelicot?Compactness?compactness_value_1d
Declares cic:/Coquelicot?Compactness cic:/Coquelicot?Compactness?compactness_value_2d
......
......@@ -94,11 +94,21 @@ dataconstructor cic:/Coquelicot?Complex?C_derive_correct
theory cic:/Coquelicot?Complex
HasMeta cic:/Coquelicot?Complex http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Complex cic:/Coq/Classes?Morphisms
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Equiv
Includes cic:/Coquelicot?Complex cic:/Coq/Reals?Rtrigo_calc
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/CompleteNormedModule
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/CompleteSpace
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/NormedModuleAux
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/ModuleSpace
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/UniformSpace
Includes cic:/Coquelicot?Complex cic:/Coq/setoid_ring?InitialRing
Includes cic:/Coquelicot?Complex cic:/Coq/ZArith?Zbool
Includes cic:/Coquelicot?Complex cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?Complex cic:/Coq/setoid_ring?Ring_theory
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/NormedModule
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/AbsRing
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/Ring
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy/AbelianGroup
Includes cic:/Coquelicot?Complex cic:/Coq/setoid_ring?Field_theory
Includes cic:/Coquelicot?Complex cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Complex cic:/Coq/Reals?Ratan
......@@ -116,7 +126,11 @@ Includes cic:/Coquelicot?Complex cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Complex cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Complex cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Complex cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Derive
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Continuity
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?Complex cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Complex cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Complex http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Coquelicot?Complex cic:/Coquelicot?Complex?C
......
......@@ -104,6 +104,21 @@ dataconstructor cic:/Coquelicot?Continuity?continuous_id
dataconstructor cic:/Coquelicot?Continuity?continuous_mult
theory cic:/Coquelicot?Continuity
HasMeta cic:/Coquelicot?Continuity http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Lub
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy/ModuleSpace
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy/Ring
Includes cic:/Coquelicot?Continuity cic:/Coq/Reals?Rsqrt_def
Includes cic:/Coquelicot?Continuity cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy/AbelianGroup
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy/NormedModule
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy/AbsRing
Includes cic:/Coquelicot?Continuity cic:/Coq/Reals?Ranalysis1
Includes cic:/Coquelicot?Continuity cic:/Coq/Reals?Rlimit
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy/UniformSpace
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Lim_seq
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Continuity cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Continuity http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Continuity cic:/Coquelicot?Compactness
......
theory cic:/Coquelicot?Coquelicot
HasMeta cic:/Coquelicot?Coquelicot http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?SF_seq
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Series
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Seq_fct
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?RInt_analysis
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?RInt_gen
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?RInt
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?PSeries
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Markov
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Lub
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Lim_seq
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?ElemFct
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Equiv
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Derive_2d
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Derive
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Continuity
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Complex
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?Compactness
Includes cic:/Coquelicot?Coquelicot cic:/Coquelicot?AutoDerive
Includes cic:/Coquelicot?Coquelicot http://coq.inria.fr/foundation?CoqSyntax
This diff is collapsed.
......@@ -32,63 +32,21 @@ dataconstructor cic:/Coquelicot?Derive_2d?DL_regular_n
dataconstructor cic:/Coquelicot?Derive_2d?Taylor_Lagrange_2d
theory cic:/Coquelicot?Derive_2d
HasMeta cic:/Coquelicot?Derive_2d http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rprod
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Cauchy_prod
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?PartSum
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Plus
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Bool?Bool
Includes cic:/Coquelicot?Derive_2d cic:/Coq/ssr?ssrbool
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Compare_dec
Includes cic:/Coquelicot?Derive_2d cic:/Coq/ZArith?Znat
Includes cic:/Coquelicot?Derive_2d cic:/Coq/ZArith?auxiliary
Includes cic:/Coquelicot?Derive_2d cic:/Coq/omega?OmegaLemmas
Includes cic:/Coquelicot?Derive_2d cic:/Coq/ZArith?BinInt
Includes cic:/Coquelicot?Derive_2d cic:/Coq/ZArith?Znat/Nat2Z
Includes cic:/Coquelicot?Derive_2d cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Peano_dec
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Logic?Decidable
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Minus
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Gt
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Lt
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Le
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Init?Peano
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rlimit
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Arith?Factorial
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Init?Nat
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Binomial
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rfunctions
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?EnvRing
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?RMicromega
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?Tauto
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?VarMap
Includes cic:/Coquelicot?Derive_2d cic:/Coq/QArith?QArith_base
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?RingMicromega
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?QMicromega
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Ranalysis1
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rpow_def
Includes cic:/Coquelicot?Derive_2d cic:/Coq/NArith?BinNat/N
Includes cic:/Coquelicot?Derive_2d cic:/Coq/setoid_ring?Field_theory
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Derive_2d cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?Derive_2d cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?DiscrR
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Classes?Morphisms
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rtrigo_calc
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?R_sqrt
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Derive
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Continuity
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?Psatz
Includes cic:/Coquelicot?Derive_2d cic:/Coq/omega?Omega
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy/AbelianGroup
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy/NormedModuleAux
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy/AbsRing
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy/ModuleSpace
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Equiv
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy/NormedModule
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy/UniformSpace
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Derive_2d cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Derive_2d cic:/Coq/omega?Omega
Includes cic:/Coquelicot?Derive_2d cic:/Coq/micromega?Psatz
Includes cic:/Coquelicot?Derive_2d http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Continuity
Includes cic:/Coquelicot?Derive_2d cic:/Coquelicot?Derive
Declares cic:/Coquelicot?Derive_2d cic:/Coquelicot?Derive_2d?differentiable_pt_lim
constant cic:/Coquelicot?Derive_2d?differentiable_pt_lim
Declares cic:/Coquelicot?Derive_2d cic:/Coquelicot?Derive_2d?filterdiff_differentiable_pt_lim
......
......@@ -15,10 +15,6 @@ dataconstructor cic:/Coquelicot?ElemFct?filterlim_sqrt_p
dataconstructor cic:/Coquelicot?ElemFct?is_lim_sqrt_p
dataconstructor cic:/Coquelicot?ElemFct?filterdiff_sqrt
dataconstructor cic:/Coquelicot?ElemFct?is_derive_sqrt
dataconstructor cic:/Coquelicot?ElemFct?nat_to_ring
dataconstructor cic:/Coquelicot?ElemFct?nat_to_ring_O
dataconstructor cic:/Coquelicot?ElemFct?nat_to_ring_Sn
dataconstructor cic:/Coquelicot?ElemFct?is_derive_mult
dataconstructor cic:/Coquelicot?ElemFct?filterdiff_pow_n
dataconstructor cic:/Coquelicot?ElemFct?is_derive_n_pow_smalli
dataconstructor cic:/Coquelicot?ElemFct?Derive_n_pow_smalli
......@@ -47,60 +43,26 @@ dataconstructor cic:/Coquelicot?ElemFct?CV_radius_atan
dataconstructor cic:/Coquelicot?ElemFct?atan_Reals
theory cic:/Coquelicot?ElemFct
HasMeta cic:/Coquelicot?ElemFct http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?AltSeries
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Ratan
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?RiemannInt
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rtrigo_reg
Includes cic:/Coquelicot?ElemFct cic:/Coq/setoid_ring?InitialRing
Includes cic:/Coquelicot?ElemFct cic:/Coq/ZArith?Zbool
Includes cic:/Coquelicot?ElemFct cic:/Coq/setoid_ring?RealField
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Ranalysis4
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Exp_prop
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rpower
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?Plus
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rprod
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rtrigo_fun
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Alembert
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rtrigo_def
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rseries
Includes cic:/Coquelicot?ElemFct cic:/Coq/ZArith?Znat
Includes cic:/Coquelicot?ElemFct cic:/Coq/ZArith?auxiliary
Includes cic:/Coquelicot?ElemFct cic:/Coq/omega?OmegaLemmas
Includes cic:/Coquelicot?ElemFct cic:/Coq/ZArith?Znat/Nat2Z
Includes cic:/Coquelicot?ElemFct cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?ElemFct cic:/Coq/Logic?Decidable
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?Compare_dec
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?ArithProp
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?Lt
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rfunctions
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?Minus
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?Factorial
Includes cic:/Coquelicot?ElemFct cic:/Coq/Init?Nat
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/Coquelicot?ElemFct cic:/Coq/Arith?Le
Includes cic:/Coquelicot?ElemFct cic:/Coq/Init?Peano
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Sqrt_reg
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?R_sqrt
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rpow_def
Includes cic:/Coquelicot?ElemFct cic:/Coq/NArith?BinNat/N
Includes cic:/Coquelicot?ElemFct cic:/Coq/setoid_ring?Field_theory
Includes cic:/Coquelicot?ElemFct cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?ElemFct cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?ElemFct cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Ranalysis1
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?ElemFct cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?ElemFct cic:/Coq/Init?Specif
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?ElemFct cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?ElemFct cic:/Coq/Init?Logic
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Derive
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Continuity
Includes cic:/Coquelicot?ElemFct cic:/Coq/omega?Omega
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Series
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Rcomplements/MyNat
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Hierarchy/Ring
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Equiv
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Hierarchy/NormedModule
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Hierarchy/AbelianGroup
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Hierarchy/UniformSpace
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Hierarchy/AbsRing
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?RInt_analysis
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Lim_seq
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?PSeries
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?RInt
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?ElemFct cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?ElemFct cic:/Coq/omega?Omega
Includes cic:/Coquelicot?ElemFct http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Continuity
Includes cic:/Coquelicot?ElemFct cic:/Coquelicot?Derive
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?continuous_abs
constant cic:/Coquelicot?ElemFct?continuous_abs
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?filterlim_abs_0
......@@ -136,13 +98,9 @@ constant cic:/Coquelicot?ElemFct?filterdiff_sqrt
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?is_derive_sqrt
constant cic:/Coquelicot?ElemFct?is_derive_sqrt
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?nat_to_ring
constant cic:/Coquelicot?ElemFct?nat_to_ring
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?nat_to_ring_O
constant cic:/Coquelicot?ElemFct?nat_to_ring_O
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?nat_to_ring_Sn
constant cic:/Coquelicot?ElemFct?nat_to_ring_Sn
deriveddeclaration cic:/Coquelicot?ElemFct?nat_to_ring
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?is_derive_mult
constant cic:/Coquelicot?ElemFct?is_derive_mult
deriveddeclaration cic:/Coquelicot?ElemFct?is_derive_mult
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?filterdiff_pow_n
constant cic:/Coquelicot?ElemFct?filterdiff_pow_n
Declares cic:/Coquelicot?ElemFct cic:/Coquelicot?ElemFct?is_derive_n_pow_smalli
......
......@@ -5,59 +5,26 @@ dataconstructor cic:/Coquelicot?Equiv?domin_trans
dataconstructor cic:/Coquelicot?Equiv?equiv_le_2
dataconstructor cic:/Coquelicot?Equiv?domin_rw_l
dataconstructor cic:/Coquelicot?Equiv?domin_rw_r
dataconstructor cic:/Coquelicot?Equiv?equiv_refl
dataconstructor cic:/Coquelicot?Equiv?equiv_sym
dataconstructor cic:/Coquelicot?Equiv?equiv_trans
dataconstructor cic:/Coquelicot?Equiv?equiv_carac_0
dataconstructor cic:/Coquelicot?Equiv?equiv_carac_1
dataconstructor cic:/Coquelicot?Equiv?equiv_ext_loc
dataconstructor cic:/Coquelicot?Equiv?is_domin_le
dataconstructor cic:/Coquelicot?Equiv?domin_scal_r
dataconstructor cic:/Coquelicot?Equiv?domin_scal_l
dataconstructor cic:/Coquelicot?Equiv?domin_plus
dataconstructor cic:/Coquelicot?Equiv?equiv_scal
dataconstructor cic:/Coquelicot?Equiv?equiv_plus
dataconstructor cic:/Coquelicot?Equiv?domin_mult_r
dataconstructor cic:/Coquelicot?Equiv?domin_mult_l
dataconstructor cic:/Coquelicot?Equiv?domin_mult
dataconstructor cic:/Coquelicot?Equiv?domin_inv
dataconstructor cic:/Coquelicot?Equiv?equiv_mult
dataconstructor cic:/Coquelicot?Equiv?equiv_inv
dataconstructor cic:/Coquelicot?Equiv?domin_comp
dataconstructor cic:/Coquelicot?Equiv?filterlim_equiv
theory cic:/Coquelicot?Equiv
HasMeta cic:/Coquelicot?Equiv http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?DiscrR
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?Ratan
Includes cic:/Coquelicot?Equiv cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Equiv cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?Equiv cic:/Coq/Classes?Morphisms
Includes cic:/Coquelicot?Equiv cic:/Coq/setoid_ring?RealField
Includes cic:/Coquelicot?Equiv cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?Equiv cic:/Coq/setoid_ring?InitialRing
Includes cic:/Coquelicot?Equiv cic:/Coq/ZArith?Zbool
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?Rpow_def
Includes cic:/Coquelicot?Equiv cic:/Coq/NArith?BinNat/N
Includes cic:/Coquelicot?Equiv cic:/Coq/setoid_ring?Field_theory
Includes cic:/Coquelicot?Equiv cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?Equiv cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?R_sqrt
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?EnvRing
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?RMicromega
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?Tauto
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?VarMap
Includes cic:/Coquelicot?Equiv cic:/Coq/QArith?QArith_base
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?RingMicromega
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?QMicromega
Includes cic:/Coquelicot?Equiv cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Equiv cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Equiv cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?Psatz
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy/UniformSpace
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy/ModuleSpace
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy/Ring
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy/AbelianGroup
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy/NormedModule
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy/AbsRing
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Equiv cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?Equiv cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Equiv cic:/Coq/micromega?Psatz
Includes cic:/Coquelicot?Equiv http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?is_domin
constant cic:/Coquelicot?Equiv?is_domin
......@@ -75,34 +42,10 @@ Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_rw_r
constant cic:/Coquelicot?Equiv?domin_rw_r
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?Equiv
deriveddeclaration cic:/Coquelicot?Equiv?Equiv
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_refl
constant cic:/Coquelicot?Equiv?equiv_refl
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_sym
constant cic:/Coquelicot?Equiv?equiv_sym
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_trans
constant cic:/Coquelicot?Equiv?equiv_trans
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_carac_0
constant cic:/Coquelicot?Equiv?equiv_carac_0
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_carac_1
constant cic:/Coquelicot?Equiv?equiv_carac_1
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_ext_loc
constant cic:/Coquelicot?Equiv?equiv_ext_loc
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?Domin
deriveddeclaration cic:/Coquelicot?Equiv?Domin
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?is_domin_le
constant cic:/Coquelicot?Equiv?is_domin_le
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_scal_r
constant cic:/Coquelicot?Equiv?domin_scal_r
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_scal_l
constant cic:/Coquelicot?Equiv?domin_scal_l
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_plus
constant cic:/Coquelicot?Equiv?domin_plus
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?Equiv_VS
deriveddeclaration cic:/Coquelicot?Equiv?Equiv_VS
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_scal
constant cic:/Coquelicot?Equiv?equiv_scal
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_plus
constant cic:/Coquelicot?Equiv?equiv_plus
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_mult_r
constant cic:/Coquelicot?Equiv?domin_mult_r
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_mult_l
......@@ -117,7 +60,5 @@ Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?equiv_inv
constant cic:/Coquelicot?Equiv?equiv_inv
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?Domin_comp
deriveddeclaration cic:/Coquelicot?Equiv?Domin_comp
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?domin_comp
constant cic:/Coquelicot?Equiv?domin_comp
Declares cic:/Coquelicot?Equiv cic:/Coquelicot?Equiv?filterlim_equiv
constant cic:/Coquelicot?Equiv?filterlim_equiv
dataconstructor cic:/Coquelicot?Iter?iter
dataconstructor cic:/Coquelicot?Iter?iter'
dataconstructor cic:/Coquelicot?Iter?iter_iter'
dataconstructor cic:/Coquelicot?Iter?iter_cat
dataconstructor cic:/Coquelicot?Iter?iter_ext
dataconstructor cic:/Coquelicot?Iter?iter_comp
dataconstructor cic:/Coquelicot?Iter?iter_const
dataconstructor cic:/Coquelicot?Iter?In_mem
dataconstructor cic:/Coquelicot?Iter?In_iota
dataconstructor cic:/Coquelicot?Iter?iter_nat
dataconstructor cic:/Coquelicot?Iter?iter_nat_ext_loc
dataconstructor cic:/Coquelicot?Iter?iter_nat_point
dataconstructor cic:/Coquelicot?Iter?iter_nat_Chasles
dataconstructor cic:/Coquelicot?Iter?iter_nat_S
theory cic:/Coquelicot?Iter
HasMeta cic:/Coquelicot?Iter http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Iter cic:/Coq/ZArith?BinInt
Includes cic:/Coquelicot?Iter cic:/Coq/Arith?Peano_dec
Includes cic:/Coquelicot?Iter cic:/Coq/Arith?Le
Includes cic:/Coquelicot?Iter cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?Iter cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/Coquelicot?Iter cic:/Coq/Arith?Minus
Includes cic:/Coquelicot?Iter cic:/Coq/ZArith?Znat
Includes cic:/Coquelicot?Iter cic:/Coq/ZArith?auxiliary
Includes cic:/Coquelicot?Iter cic:/Coq/omega?OmegaLemmas
Includes cic:/Coquelicot?Iter cic:/Coq/ZArith?Znat/Nat2Z
Includes cic:/Coquelicot?Iter cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?Iter cic:/Coq/Logic?Decidable
Includes cic:/Coquelicot?Iter cic:/Coq/Arith?Compare_dec
Includes cic:/Coquelicot?Iter cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Iter cic:/Coq/Init?Peano
Includes cic:/Coquelicot?Iter cic:/Coq/Init?Nat
Includes cic:/Coquelicot?Iter cic:/Coq/Bool?Bool
Includes cic:/Coquelicot?Iter cic:/Coq/ssr?ssrbool
Includes cic:/Coquelicot?Iter cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?Iter cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?Iter cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?Iter cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Iter cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Iter cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Iter cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Iter cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Iter cic:/Coq/omega?Omega
Includes cic:/Coquelicot?Iter cic:/Coquelicot?Rcomplements/MyNat
Includes cic:/Coquelicot?Iter cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Iter cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Iter http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Iter cic:/Coq/omega?Omega
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?Iter
deriveddeclaration cic:/Coquelicot?Iter?Iter
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter
constant cic:/Coquelicot?Iter?iter
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter'
constant cic:/Coquelicot?Iter?iter'
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_iter'
constant cic:/Coquelicot?Iter?iter_iter'
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_cat
constant cic:/Coquelicot?Iter?iter_cat
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_ext
constant cic:/Coquelicot?Iter?iter_ext
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_comp
constant cic:/Coquelicot?Iter?iter_comp
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_const
constant cic:/Coquelicot?Iter?iter_const
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?In_mem
......@@ -65,13 +18,3 @@ Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?In_iota
constant cic:/Coquelicot?Iter?In_iota
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?Iter_nat
deriveddeclaration cic:/Coquelicot?Iter?Iter_nat
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_nat
constant cic:/Coquelicot?Iter?iter_nat
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_nat_ext_loc
constant cic:/Coquelicot?Iter?iter_nat_ext_loc
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_nat_point
constant cic:/Coquelicot?Iter?iter_nat_point
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_nat_Chasles
constant cic:/Coquelicot?Iter?iter_nat_Chasles
Declares cic:/Coquelicot?Iter cic:/Coquelicot?Iter?iter_nat_S
constant cic:/Coquelicot?Iter?iter_nat_S
......@@ -40,6 +40,7 @@ Includes cic:/Coquelicot?KHInt cic:/Coq/Classes?Morphisms
Includes cic:/Coquelicot?KHInt cic:/Coq/Reals?DiscrR
Includes cic:/Coquelicot?KHInt cic:/Coq/ssr?ssrbool
Includes cic:/Coquelicot?KHInt cic:/Coq/Arith?Le
Includes cic:/Coquelicot?KHInt cic:/Coquelicot?Rcomplements/MyNat
Includes cic:/Coquelicot?KHInt cic:/Coq/Arith?Compare_dec
Includes cic:/Coquelicot?KHInt cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?KHInt cic:/Coq/Init?Nat
......@@ -54,7 +55,10 @@ Includes cic:/Coquelicot?KHInt cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?KHInt cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?KHInt cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?KHInt cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?KHInt cic:/Coquelicot?RInt
Includes cic:/Coquelicot?KHInt cic:/Coquelicot?SF_seq
Includes cic:/Coquelicot?KHInt cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?KHInt cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?KHInt cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?KHInt http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Coquelicot?KHInt cic:/Coquelicot?KHInt?ith_step
......
......@@ -177,62 +177,15 @@ dataconstructor cic:/Coquelicot?Lim_seq?ex_lim_seq_geom_m
dataconstructor cic:/Coquelicot?Lim_seq?is_lim_seq_Rbar_loc_seq
theory cic:/Coquelicot?Lim_seq
HasMeta cic:/Coquelicot?Lim_seq http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Cos_rel
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Rprod
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Ranalysis1
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?EnvRing
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?RMicromega
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?Tauto
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?VarMap
Includes cic:/Coquelicot?Lim_seq cic:/Coq/QArith?QArith_base
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?RingMicromega
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?QMicromega
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Hierarchy/AbsRing
Includes cic:/Coquelicot?Lim_seq cic:/Coq/setoid_ring?RealField
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?Minus
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?Lt
Includes cic:/Coquelicot?Lim_seq cic:/Coq/setoid_ring?InitialRing
Includes cic:/Coquelicot?Lim_seq cic:/Coq/ZArith?Zbool
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Program?Basics
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Classes?Morphisms_Prop
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?SeqProp
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Rfunctions
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Rseries
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Hierarchy/UniformSpace
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?DiscrR
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?Gt
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?Le
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/Coquelicot?Lim_seq cic:/Coq/ZArith?Znat
Includes cic:/Coquelicot?Lim_seq cic:/Coq/ZArith?auxiliary
Includes cic:/Coquelicot?Lim_seq cic:/Coq/omega?OmegaLemmas
Includes cic:/Coquelicot?Lim_seq cic:/Coq/ZArith?Znat/Nat2Z
Includes cic:/Coquelicot?Lim_seq cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?Compare_dec
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Logic?Decidable
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Classes?RelationClasses
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Classes?Morphisms
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Arith?Plus
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Init?Nat
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Init?Peano
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Rpow_def
Includes cic:/Coquelicot?Lim_seq cic:/Coq/NArith?BinNat/N
Includes cic:/Coquelicot?Lim_seq cic:/Coq/setoid_ring?Field_theory
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Lim_seq cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?Lim_seq cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Lim_seq cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Hierarchy
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?Psatz
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Rcomplements/MyNat
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Markov
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Lub
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Lim_seq cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Lim_seq cic:/Coq/micromega?Psatz
Includes cic:/Coquelicot?Lim_seq http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Lim_seq cic:/Coquelicot?Hierarchy
Declares cic:/Coquelicot?Lim_seq cic:/Coquelicot?Lim_seq?is_sup_seq
constant cic:/Coquelicot?Lim_seq?is_sup_seq
Declares cic:/Coquelicot?Lim_seq cic:/Coquelicot?Lim_seq?is_inf_seq
......
......@@ -75,16 +75,9 @@ dataconstructor cic:/Coquelicot?Lub?not_Empty_dec
dataconstructor cic:/Coquelicot?Lub?uniqueness_dec
theory cic:/Coquelicot?Lub
HasMeta cic:/Coquelicot?Lub http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Lub cic:/Coq/Logic?Decidable
Includes cic:/Coquelicot?Lub cic:/Coq/ssr?ssreflect
Includes cic:/Coquelicot?Lub cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Lub cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Lub cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Lub cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Lub cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Lub cic:/Coq/Reals?RIneq
Includes cic:/Coquelicot?Lub cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Lub cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Lub cic:/Coquelicot?Markov
Includes cic:/Coquelicot?Lub cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Lub cic:/Coquelicot?Rbar
Includes cic:/Coquelicot?Lub cic:/Coq/Reals?Reals
Includes cic:/Coquelicot?Lub http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Coquelicot?Lub cic:/Coquelicot?Lub?is_ub_Rbar
......
......@@ -8,36 +8,9 @@ dataconstructor cic:/Coquelicot?Markov?EM_dec
dataconstructor cic:/Coquelicot?Markov?EM_dec'
theory cic:/Coquelicot?Markov
HasMeta cic:/Coquelicot?Markov http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Coquelicot?Markov cic:/Coq/Reals?Rbasic_fun
Includes cic:/Coquelicot?Markov cic:/Coq/Bool?Bool
Includes cic:/Coquelicot?Markov cic:/Coq/ssr?ssrbool
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?Znat
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?auxiliary
Includes cic:/Coquelicot?Markov cic:/Coq/omega?OmegaLemmas
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?Znat/Nat2Z
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?BinInt
Includes cic:/Coquelicot?Markov cic:/Coq/Arith?Compare_dec
Includes cic:/Coquelicot?Markov cic:/Coq/Logic?Decidable
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?Znat/Zabs2Nat
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?Zorder
Includes cic:/Coquelicot?Markov cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Coquelicot?Markov cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Coquelicot?Markov cic:/Coq/ZArith?BinInt/Z
Includes cic:/Coquelicot?Markov cic:/Coq/Init?Peano
Includes cic:/Coquelicot?Markov cic:/Coq/Init?Specif
Includes cic:/Coquelicot?Markov cic:/Coq/Arith?Le
Includes cic:/Coquelicot?Markov cic:/Coq/Classes?RelationClasses
Includes cic:/Coquelicot?Markov cic:/Coq/Program?Basics
Includes cic:/Coquelicot?Markov cic:/Coq/Classes?Morphisms
Includes cic:/Coquelicot?Markov cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/Coquelicot?Markov cic:/Coq/Numbers?BinNums
Includes cic:/Coquelicot?Markov cic:/Coq/Reals?Raxioms
Includes cic:/Coquelicot?Markov cic:/Coq/Reals?Rdefinitions
Includes cic:/Coquelicot?Markov cic:/Coq/Init?Logic
Includes cic:/Coquelicot?Markov cic:/Coq/Init?Datatypes
Includes cic:/Coquelicot?Markov cic:/Coq/omega?Omega
Includes cic:/Coquelicot?Markov cic:/Coquelicot?Rcomplements
Includes cic:/Coquelicot?Markov cic:/Coq/Reals?RIneq