Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13564 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (95 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (211 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (71 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6947 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (305 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (352 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (295 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (183 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2870 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (287 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (433 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1189 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (326 entries)

P (definition)

PairDecidableType.eq [in Coq.Logic.DecidableTypeEx]
PairDecidableType.eq_dec [in Coq.Logic.DecidableTypeEx]
PairDecidableType.t [in Coq.Logic.DecidableTypeEx]
PairOrderedType.compare [in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq [in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq_dec [in Coq.FSets.OrderedTypeEx]
PairOrderedType.lt [in Coq.FSets.OrderedTypeEx]
PairOrderedType.t [in Coq.FSets.OrderedTypeEx]
PairUsualDecidableType.eq [in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_dec [in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_refl [in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_sym [in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_trans [in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.t [in Coq.Logic.DecidableTypeEx]
partition [in Coq.Lists.List]
Pbit [in Coq.NArith.Ndigits]
Pcompare [in Coq.Arith.Compare]
Pcompare [in Coq.NArith.BinPos]
Pdiv [in Coq.Numbers.Natural.BigN.Nbasic]
Pdiv2 [in Coq.NArith.BinPos]
Pdiv_eucl [in Coq.ZArith.ZOdiv_def]
Pdouble_mask [in Coq.NArith.BinPos]
Pdouble_minus_one [in Coq.NArith.BinPos]
Pdouble_minus_two [in Coq.NArith.BinPos]
Pdouble_plus_one_mask [in Coq.NArith.BinPos]
peanoView [in Coq.NArith.BinPos]
PeanoView_iter [in Coq.NArith.BinPos]
peanoView_xI [in Coq.NArith.BinPos]
peanoView_xO [in Coq.NArith.BinPos]
Peqb [in Coq.NArith.Ndec]
pequiv [in Coq.Classes.Equivalence]
permutation [in Coq.Sorting.Permutation]
Pgcd [in Coq.ZArith.Znumtheory]
Pgcdn [in Coq.ZArith.Znumtheory]
Pge [in Coq.NArith.BinPos]
Pggcd [in Coq.ZArith.Znumtheory]
Pggcdn [in Coq.ZArith.Znumtheory]
Pgt [in Coq.NArith.BinPos]
phi [in Coq.Numbers.Cyclic.Int31.Int31]
Phi [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi2 [in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv [in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv2 [in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv_positive [in Coq.Numbers.Cyclic.Int31.Int31]
phi_sequence [in Coq.Reals.RiemannInt]
PI [in Coq.Reals.AltSeries]
Pind [in Coq.NArith.BinPos]
PI.proof_irrelevance [in Coq.Logic.ProofIrrelevance]
PI_tg [in Coq.Reals.AltSeries]
plat [in Coq.Reals.Rtrigo_calc]
Ple [in Coq.NArith.BinPos]
plength [in Coq.Numbers.Natural.BigN.Nbasic]
Plt [in Coq.NArith.BinPos]
plus [in Coq.Init.Peano]
plusnS [in Coq.Numbers.Natural.BigN.Nbasic]
plusn0 [in Coq.Numbers.Natural.BigN.Nbasic]
plus_fct [in Coq.Reals.Ranalysis1]
plus_is_one [in Coq.Arith.Plus]
Pmax [in Coq.NArith.BinPos]
Pmin [in Coq.NArith.BinPos]
Pminus [in Coq.NArith.BinPos]
Pminus_mask [in Coq.NArith.BinPos]
Pminus_mask_carry [in Coq.NArith.BinPos]
Pmult [in Coq.NArith.BinPos]
Pmult_nat [in Coq.NArith.BinPos]
pointwise_extension [in Coq.Classes.RelationClasses]
pointwise_lifting [in Coq.Classes.RelationClasses]
pointwise_relation [in Coq.Classes.Morphisms]
point_adherent [in Coq.Reals.Rtopology]
PositiveMap.add [in Coq.FSets.FMapPositive]
PositiveMap.cardinal [in Coq.FSets.FMapPositive]
PositiveMap.elements [in Coq.FSets.FMapPositive]
PositiveMap.Empty [in Coq.FSets.FMapPositive]
PositiveMap.empty [in Coq.FSets.FMapPositive]
PositiveMap.equal [in Coq.FSets.FMapPositive]
PositiveMap.Equal [in Coq.FSets.FMapPositive]
PositiveMap.Equiv [in Coq.FSets.FMapPositive]
PositiveMap.Equivb [in Coq.FSets.FMapPositive]
PositiveMap.eq_key [in Coq.FSets.FMapPositive]
PositiveMap.eq_key_elt [in Coq.FSets.FMapPositive]
PositiveMap.find [in Coq.FSets.FMapPositive]
PositiveMap.fold [in Coq.FSets.FMapPositive]
PositiveMap.In [in Coq.FSets.FMapPositive]
PositiveMap.is_empty [in Coq.FSets.FMapPositive]
PositiveMap.key [in Coq.FSets.FMapPositive]
PositiveMap.lt_key [in Coq.FSets.FMapPositive]
PositiveMap.map [in Coq.FSets.FMapPositive]
PositiveMap.mapi [in Coq.FSets.FMapPositive]
PositiveMap.MapsTo [in Coq.FSets.FMapPositive]
PositiveMap.map2 [in Coq.FSets.FMapPositive]
PositiveMap.mem [in Coq.FSets.FMapPositive]
PositiveMap.remove [in Coq.FSets.FMapPositive]
PositiveMap.t [in Coq.FSets.FMapPositive]
PositiveMap.xelements [in Coq.FSets.FMapPositive]
PositiveMap.xfind [in Coq.FSets.FMapPositive]
PositiveMap.xfoldi [in Coq.FSets.FMapPositive]
PositiveMap.xmapi [in Coq.FSets.FMapPositive]
PositiveMap.xmap2_l [in Coq.FSets.FMapPositive]
PositiveMap.xmap2_r [in Coq.FSets.FMapPositive]
PositiveMap._map2 [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.compare [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_refl [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_sym [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_trans [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.t [in Coq.FSets.FMapPositive]
Positive_as_OT.compare [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_dec [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_refl [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_sym [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_trans [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.lt [in Coq.FSets.OrderedTypeEx]
Positive_as_OT.t [in Coq.FSets.OrderedTypeEx]
positive_to_int31 [in Coq.Numbers.Cyclic.Int31.Int31]
positivity_seq [in Coq.Reals.AltSeries]
pos_mod [in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
pos_Rl [in Coq.Reals.RList]
Pow [in Coq.Relations.Relation_Operators]
pow [in Coq.Logic.Berardi]
pow [in Coq.Reals.Rpow_def]
powerRZ [in Coq.Reals.Rfunctions]
Power_set_PO [in Coq.Sets.Powerset]
pow_fct [in Coq.Reals.Ranalysis1]
pow_2_n [in Coq.Reals.Rsqrt_def]
Pplength [in Coq.NArith.Ndist]
Pplus [in Coq.NArith.BinPos]
Pplus_carry [in Coq.NArith.BinPos]
Ppred [in Coq.NArith.BinPos]
Ppred_mask [in Coq.NArith.BinPos]
Prec [in Coq.NArith.BinPos]
Prect [in Coq.NArith.BinPos]
pred [in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
pred [in Coq.Init.Peano]
predicate [in Coq.Numbers.NumPrelude]
PredicateExtensionality [in Coq.Logic.Diaconescu]
predicate_all [in Coq.Classes.RelationClasses]
predicate_equivalence [in Coq.Classes.RelationClasses]
predicate_exists [in Coq.Classes.RelationClasses]
predicate_implication [in Coq.Classes.RelationClasses]
predicate_intersection [in Coq.Classes.RelationClasses]
predicate_union [in Coq.Classes.RelationClasses]
predicate_wd [in Coq.Numbers.NumPrelude]
pred_c [in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
prefix [in Coq.Strings.String]
prime' [in Coq.ZArith.Znumtheory]
prime_dec [in Coq.ZArith.Znumtheory]
prime_dec_aux [in Coq.ZArith.Znumtheory]
primitive [in Coq.Reals.RiemannInt]
prod_curry [in Coq.Init.Datatypes]
prod_f_R0 [in Coq.Reals.Rprod]
prod_rel [in Coq.Numbers.NumPrelude]
prod_uncurry [in Coq.Init.Datatypes]
proj [in Coq.Logic.Eqdep_dec]
projT1 [in Coq.Init.Specif]
projT2 [in Coq.Init.Specif]
proj1_inf [in Coq.Logic.ChoiceFacts]
proj1_sig [in Coq.Init.Specif]
proj2_sig [in Coq.Init.Specif]
ProofIrrelevance [in Coq.Logic.ChoiceFacts]
proof_irrelevance [in Coq.Logic.ClassicalFacts]
prop_degeneracy [in Coq.Logic.ClassicalFacts]
prop_extensionality [in Coq.Logic.ClassicalFacts]
provable_prop_extensionality [in Coq.Logic.ClassicalFacts]
Pser [in Coq.Reals.Rseries]
Psize [in Coq.NArith.BinPos]
Psquare [in Coq.ZArith.Zpow_facts]
Psucc [in Coq.NArith.BinPos]
Ptail [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Pxor [in Coq.NArith.Ndigits]
P' [in Coq.Logic.ConstructiveEpsilon]
p2b [in Coq.Logic.ClassicalFacts]
P2Bv [in Coq.NArith.Ndigits]
p2i [in Coq.Numbers.Cyclic.Int31.Int31]
p2ibis [in Coq.Numbers.Cyclic.Int31.Cyclic31]
P_of_succ_nat [in Coq.NArith.BinPos]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13564 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (95 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (211 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (71 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6947 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (305 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (352 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (295 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (183 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2870 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (287 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (433 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1189 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (326 entries)