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 | _ | other | (22221 entries) |

Notation 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 | _ | other | (923 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 | _ | other | (744 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 | _ | other | (1480 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 | _ | other | (501 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 | _ | other | (10364 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 | _ | other | (910 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 | _ | other | (573 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 | _ | other | (386 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 | _ | other | (286 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 | _ | other | (465 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 | _ | other | (632 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 | _ | other | (1133 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 | _ | other | (3679 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 | _ | other | (145 entries) |

## P (constructor)

PackKeyedPred [in Coq.ssr.ssrbool]PackKeyedQualifier [in Coq.ssr.ssrbool]

pair [in Coq.Init.Datatypes]

partial_order_equivalence [in Coq.Classes.CRelationClasses]

partial_order_equivalence [in Coq.Classes.RelationClasses]

Pc [in Coq.micromega.EnvRing]

Pc [in Coq.setoid_ring.Ncring_polynom]

Pc [in Coq.setoid_ring.Ring_polynom]

PEadd [in Coq.micromega.EnvRing]

PEadd [in Coq.setoid_ring.Ring_polynom]

PEc [in Coq.micromega.EnvRing]

PEc [in Coq.setoid_ring.Ring_polynom]

PEI [in Coq.setoid_ring.Ring_polynom]

PEmul [in Coq.micromega.EnvRing]

PEmul [in Coq.setoid_ring.Ring_polynom]

PEO [in Coq.setoid_ring.Ring_polynom]

PEopp [in Coq.micromega.EnvRing]

PEopp [in Coq.setoid_ring.Ring_polynom]

PEpow [in Coq.micromega.EnvRing]

PEpow [in Coq.setoid_ring.Ring_polynom]

permA_trans [in Coq.Lists.SetoidPermutation]

permA_swap [in Coq.Lists.SetoidPermutation]

permA_skip [in Coq.Lists.SetoidPermutation]

permA_nil [in Coq.Lists.SetoidPermutation]

perm_trans [in Coq.Sorting.Permutation]

perm_swap [in Coq.Sorting.Permutation]

perm_skip [in Coq.Sorting.Permutation]

perm_nil [in Coq.Sorting.Permutation]

PEsub [in Coq.micromega.EnvRing]

PEsub [in Coq.setoid_ring.Ring_polynom]

PEX [in Coq.micromega.EnvRing]

PEX [in Coq.setoid_ring.Ring_polynom]

Phant [in Coq.ssr.ssreflect]

Phantom [in Coq.ssr.ssreflect]

Pinj [in Coq.micromega.EnvRing]

Pinj [in Coq.setoid_ring.Ring_polynom]

PNone [in Coq.rtauto.Bintree]

Poly [in Coq.btauto.Algebra]

Pos [in Coq.Init.Decimal]

PositiveMap.Leaf [in Coq.FSets.FMapPositive]

PositiveMap.Node [in Coq.FSets.FMapPositive]

PositiveSet.ct_lgx [in Coq.FSets.FSetPositive]

PositiveSet.ct_glx [in Coq.FSets.FSetPositive]

PositiveSet.ct_exx [in Coq.FSets.FSetPositive]

PositiveSet.ct_xex [in Coq.FSets.FSetPositive]

PositiveSet.ct_xxx [in Coq.FSets.FSetPositive]

PositiveSet.ct_lgx [in Coq.MSets.MSetPositive]

PositiveSet.ct_glx [in Coq.MSets.MSetPositive]

PositiveSet.ct_exx [in Coq.MSets.MSetPositive]

PositiveSet.ct_xex [in Coq.MSets.MSetPositive]

PositiveSet.ct_xxx [in Coq.MSets.MSetPositive]

PositiveSet.Leaf [in Coq.FSets.FSetPositive]

PositiveSet.Leaf [in Coq.MSets.MSetPositive]

PositiveSet.Node [in Coq.FSets.FSetPositive]

PositiveSet.Node [in Coq.MSets.MSetPositive]

Pos.IsNeg [in Coq.PArith.BinPosDef]

Pos.IsNul [in Coq.PArith.BinPosDef]

Pos.IsPos [in Coq.PArith.BinPosDef]

Pos.PeanoOne [in Coq.PArith.BinPos]

Pos.PeanoSucc [in Coq.PArith.BinPos]

Pos.SqrtApprox [in Coq.PArith.BinPos]

Pos.SqrtExact [in Coq.PArith.BinPos]

Pos.SubIsNeg [in Coq.PArith.BinPos]

Pos.SubIsNul [in Coq.PArith.BinPos]

Pos.SubIsPos [in Coq.PArith.BinPos]

power [in Coq.setoid_ring.Algebra_syntax]

PredType [in Coq.ssr.ssrbool]

prime_intro [in Coq.ZArith.Znumtheory]

propagate [in Coq.Logic.WeakFan]

propagate_at [in Coq.Logic.WKL]

proper_proxy [in Coq.Classes.Morphisms]

proper_prf [in Coq.Classes.Morphisms]

proper_proxy [in Coq.Classes.CMorphisms]

proper_prf [in Coq.Classes.CMorphisms]

Props.BSLeaf [in Coq.MSets.MSetGenTree]

Props.BSNode [in Coq.MSets.MSetGenTree]

Props.InLeft [in Coq.MSets.MSetGenTree]

Props.InRight [in Coq.MSets.MSetGenTree]

Props.IsRoot [in Coq.MSets.MSetGenTree]

Props.ok [in Coq.MSets.MSetGenTree]

PsatzAdd [in Coq.micromega.RingMicromega]

PsatzC [in Coq.micromega.RingMicromega]

PsatzIn [in Coq.micromega.RingMicromega]

PsatzMulC [in Coq.micromega.RingMicromega]

PsatzMulE [in Coq.micromega.RingMicromega]

PsatzSquare [in Coq.micromega.RingMicromega]

PsatzZ [in Coq.micromega.RingMicromega]

PSome [in Coq.rtauto.Bintree]

PX [in Coq.micromega.EnvRing]

PX [in Coq.setoid_ring.Ncring_polynom]

PX [in Coq.setoid_ring.Ring_polynom]

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 | _ | other | (22221 entries) |

Notation 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 | _ | other | (923 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 | _ | other | (744 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 | _ | other | (1480 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 | _ | other | (501 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 | _ | other | (10364 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 | _ | other | (910 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 | _ | other | (573 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 | _ | other | (386 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 | _ | other | (286 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 | _ | other | (465 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 | _ | other | (632 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 | _ | other | (1133 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 | _ | other | (3679 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 | _ | other | (145 entries) |