| 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 | (68863 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 | (985 entries) |
| Binder 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 | (44709 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 | (761 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 | (1497 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 | (570 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 | (11380 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 | (976 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 | (603 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 | (298 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 | (460 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 | (476 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 | (811 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 | (1157 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 | (4018 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 | (162 entries) |
O (lemma)
Odd_equiv [in Coq.Numbers.Natural.Peano.NPeano]odd_S2n [in Coq.Arith.Div2]
odd_double [in Coq.Arith.Div2]
odd_div2 [in Coq.Arith.Div2]
odd_mult_inv_r [in Coq.Arith.Even]
odd_mult_inv_l [in Coq.Arith.Even]
odd_mult [in Coq.Arith.Even]
odd_plus_odd_inv_r [in Coq.Arith.Even]
odd_plus_odd_inv_l [in Coq.Arith.Even]
odd_plus_even_inv_r [in Coq.Arith.Even]
odd_plus_even_inv_l [in Coq.Arith.Even]
odd_even_plus [in Coq.Arith.Even]
odd_plus_r [in Coq.Arith.Even]
odd_plus_l [in Coq.Arith.Even]
odd_plus_split [in Coq.Arith.Even]
odd_equiv [in Coq.Arith.Even]
odd_even_lem [in Coq.Arith.Mult]
of_bits_to_bits [in Coq.Init.Byte]
of_decimal_dnormf [in Coq.Numbers.DecimalQ]
of_decimal_dnorme [in Coq.Numbers.DecimalQ]
of_to [in Coq.Numbers.DecimalQ]
of_Z_spec [in Coq.Numbers.Cyclic.Int63.Int63]
of_pos_rec_spec [in Coq.Numbers.Cyclic.Int63.Int63]
of_voidK [in Coq.ssr.ssrfun]
of_int_iter_D0 [in Coq.Numbers.DecimalZ]
of_uint_iter_D0 [in Coq.Numbers.DecimalZ]
of_iff [in Coq.Numbers.DecimalZ]
of_inj [in Coq.Numbers.DecimalZ]
of_int_norm [in Coq.Numbers.DecimalZ]
of_to [in Coq.Numbers.DecimalZ]
of_hex_int_double [in Coq.Numbers.HexadecimalZ]
of_hex_int_iter_D0 [in Coq.Numbers.HexadecimalZ]
of_hex_uint_iter_D0 [in Coq.Numbers.HexadecimalZ]
of_iff [in Coq.Numbers.HexadecimalZ]
of_inj [in Coq.Numbers.HexadecimalZ]
of_int_norm [in Coq.Numbers.HexadecimalZ]
of_to [in Coq.Numbers.HexadecimalZ]
of_nat_to_nat_inv [in Coq.Vectors.Fin]
of_nat_ext [in Coq.Vectors.Fin]
of_nat_via_N [in Coq.Strings.Byte]
of_N_via_nat [in Coq.Strings.Byte]
of_N_None_iff [in Coq.Strings.Byte]
of_to_N [in Coq.Strings.Byte]
of_nat_None_iff [in Coq.Strings.Byte]
of_to_nat [in Coq.Strings.Byte]
of_iff [in Coq.Numbers.HexadecimalQ]
of_inj [in Coq.Numbers.HexadecimalQ]
of_hexadecimal_hnorme [in Coq.Numbers.HexadecimalQ]
of_to [in Coq.Numbers.HexadecimalQ]
of_nat_to_nat_eq [in Coq.micromega.ZifyInst]
OMEGA1 [in Coq.omega.OmegaLemmas]
OMEGA10 [in Coq.omega.OmegaLemmas]
OMEGA11 [in Coq.omega.OmegaLemmas]
OMEGA12 [in Coq.omega.OmegaLemmas]
OMEGA13 [in Coq.omega.OmegaLemmas]
OMEGA14 [in Coq.omega.OmegaLemmas]
OMEGA15 [in Coq.omega.OmegaLemmas]
OMEGA16 [in Coq.omega.OmegaLemmas]
OMEGA17 [in Coq.omega.OmegaLemmas]
OMEGA18 [in Coq.omega.OmegaLemmas]
OMEGA19 [in Coq.omega.OmegaLemmas]
OMEGA2 [in Coq.omega.OmegaLemmas]
OMEGA20 [in Coq.omega.OmegaLemmas]
OMEGA3 [in Coq.omega.OmegaLemmas]
OMEGA4 [in Coq.omega.OmegaLemmas]
OMEGA5 [in Coq.omega.OmegaLemmas]
OMEGA6 [in Coq.omega.OmegaLemmas]
OMEGA7 [in Coq.omega.OmegaLemmas]
OMEGA8 [in Coq.omega.OmegaLemmas]
OMEGA9 [in Coq.omega.OmegaLemmas]
omniscient_fun_choice_imp_fun_choice [in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_small_drinker [in Coq.Logic.ChoiceFacts]
one_IZR_r_R1 [in Coq.Reals.RIneq]
one_IZR_lt1 [in Coq.Reals.RIneq]
onT_bij [in Coq.ssr.ssrbool]
onW_bij [in Coq.ssr.ssrbool]
on_can_inj [in Coq.ssr.ssrbool]
on1lT [in Coq.ssr.ssrbool]
on1lW [in Coq.ssr.ssrbool]
on1T [in Coq.ssr.ssrbool]
on1W [in Coq.ssr.ssrbool]
on2T [in Coq.ssr.ssrbool]
on2W [in Coq.ssr.ssrbool]
OpAdd_sound [in Coq.micromega.RingMicromega]
open_set_P6 [in Coq.Reals.Rtopology]
open_set_P5 [in Coq.Reals.Rtopology]
open_set_P4 [in Coq.Reals.Rtopology]
open_set_P3 [in Coq.Reals.Rtopology]
open_set_P2 [in Coq.Reals.Rtopology]
open_set_P1 [in Coq.Reals.Rtopology]
OpMult_sound [in Coq.micromega.RingMicromega]
oppcarry_spec [in Coq.Numbers.Cyclic.Int63.Int63]
oppc_spec [in Coq.Numbers.Cyclic.Int63.Int63]
opp_spec [in Coq.Numbers.Cyclic.Int63.Int63]
opp_IZR [in Coq.Reals.RIneq]
opp_inject_Z [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
opp_inject_Q [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
op_rotate [in Coq.Sets.Permut]
orbA [in Coq.ssr.ssrbool]
orbAC [in Coq.ssr.ssrbool]
orbACA [in Coq.ssr.ssrbool]
orbb [in Coq.ssr.ssrbool]
orbC [in Coq.ssr.ssrbool]
orbCA [in Coq.ssr.ssrbool]
orbF [in Coq.ssr.ssrbool]
orbK [in Coq.ssr.ssrbool]
orbN [in Coq.ssr.ssrbool]
orbT [in Coq.ssr.ssrbool]
orb_id2r [in Coq.ssr.ssrbool]
orb_id2l [in Coq.ssr.ssrbool]
orb_idr [in Coq.ssr.ssrbool]
orb_idl [in Coq.ssr.ssrbool]
orb_andr [in Coq.ssr.ssrbool]
orb_andl [in Coq.ssr.ssrbool]
orb_lazy_alt [in Coq.Bool.Bool]
orb_prop_intro [in Coq.Bool.Bool]
orb_prop_elim [in Coq.Bool.Bool]
orb_andb_distrib_l [in Coq.Bool.Bool]
orb_andb_distrib_r [in Coq.Bool.Bool]
orb_assoc [in Coq.Bool.Bool]
orb_comm [in Coq.Bool.Bool]
orb_negb_l [in Coq.Bool.Bool]
orb_negb_r [in Coq.Bool.Bool]
orb_false_l [in Coq.Bool.Bool]
orb_false_r [in Coq.Bool.Bool]
orb_true_l [in Coq.Bool.Bool]
orb_true_r [in Coq.Bool.Bool]
orb_diag [in Coq.Bool.Bool]
orb_false_elim [in Coq.Bool.Bool]
orb_false_intro [in Coq.Bool.Bool]
orb_true_intro [in Coq.Bool.Bool]
orb_prop [in Coq.Bool.Bool]
orb_true_elim [in Coq.Bool.Bool]
orb_false_iff [in Coq.Bool.Bool]
orb_true_iff [in Coq.Bool.Bool]
OrderedTypeFacts.elim_compare_gt [in Coq.Structures.OrderedType]
OrderedTypeFacts.elim_compare_lt [in Coq.Structures.OrderedType]
OrderedTypeFacts.elim_compare_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb_alt [in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb_alt [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_not_gt [in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_not_lt [in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_neq [in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_le [in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_lt [in Coq.Structures.OrderedType]
OrderedTypeFacts.gt_not_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.if_eq_dec [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.Inf_alt [in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_lt [in Coq.Structures.OrderedType]
OrderedTypeFacts.In_Inf [in Coq.Structures.OrderedType]
OrderedTypeFacts.In_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.le_lteq [in Coq.Structures.OrderedType]
OrderedTypeFacts.le_antisym [in Coq.Structures.OrderedType]
OrderedTypeFacts.le_trans [in Coq.Structures.OrderedType]
OrderedTypeFacts.le_neq [in Coq.Structures.OrderedType]
OrderedTypeFacts.le_lt_trans [in Coq.Structures.OrderedType]
OrderedTypeFacts.le_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.ListIn_Inf [in Coq.Structures.OrderedType]
OrderedTypeFacts.ListIn_In [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_dec [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_not_gt [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_le [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_le_trans [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_total [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_antirefl [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_dec [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.neq_sym [in Coq.Structures.OrderedType]
OrderedTypeFacts.neq_eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.Sort_NoDup [in Coq.Structures.OrderedType]
OrderedTypeFacts.Sort_Inf_In [in Coq.Structures.OrderedType]
OrderedTypeFullFacts.compare_ge_iff [in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.compare_le_iff [in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.eq_is_le_ge [in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_or_gt [in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_not_gt_iff [in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_or_ge [in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_not_ge_iff [in Coq.Structures.OrdersFacts]
OrderedTypeLists.Inf_alt [in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_eq [in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_lt [in Coq.Structures.OrdersLists]
OrderedTypeLists.In_Inf [in Coq.Structures.OrdersLists]
OrderedTypeLists.In_eq [in Coq.Structures.OrdersLists]
OrderedTypeLists.ListIn_Inf [in Coq.Structures.OrdersLists]
OrderedTypeLists.ListIn_In [in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort_NoDup [in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort_Inf_In [in Coq.Structures.OrdersLists]
OrderedTypeRev.compare_spec [in Coq.Structures.OrdersFacts]
OrderedTypeRev.le_lteq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_is_nlt_ngt [in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_not_gt [in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_not_lt [in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_neq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_le [in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_lt [in Coq.Structures.OrdersFacts]
OrderedTypeTest.gt_not_eq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_neq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_antisym [in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_trans [in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_lt_trans [in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_eq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_not_gt [in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_le [in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_le_trans [in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_eq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_not_eq [in Coq.Structures.OrdersFacts]
OrderedTypeTest.neq_sym [in Coq.Structures.OrdersFacts]
OrderedTypeTest.neq_eq [in Coq.Structures.OrdersFacts]
OrderedType_to_Alt.compare_trans [in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.compare_sym [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_not_eq [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_sym [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_refl [in Coq.Structures.OrderedTypeAlt]
OrderFacts.eq_neq [in Coq.Structures.OrdersTac]
OrderFacts.eq_sym [in Coq.Structures.OrdersTac]
OrderFacts.eq_refl [in Coq.Structures.OrdersTac]
OrderFacts.le_neq_lt [in Coq.Structures.OrdersTac]
OrderFacts.le_antisym [in Coq.Structures.OrdersTac]
OrderFacts.le_refl [in Coq.Structures.OrdersTac]
OrderFacts.lt_irrefl [in Coq.Structures.OrdersTac]
OrderFacts.neq_eq [in Coq.Structures.OrdersTac]
OrderFacts.neq_sym [in Coq.Structures.OrdersTac]
OrderFacts.not_gt_le [in Coq.Structures.OrdersTac]
OrderFacts.not_ge_lt [in Coq.Structures.OrdersTac]
OrderFacts.not_neq_eq [in Coq.Structures.OrdersTac]
OrderFacts.trans [in Coq.Structures.OrdersTac]
OrdProperties.add_fold [in Coq.MSets.MSetProperties]
OrdProperties.add_fold [in Coq.FSets.FSetProperties]
OrdProperties.choose_equal [in Coq.MSets.MSetProperties]
OrdProperties.choose_equal [in Coq.FSets.FSetProperties]
OrdProperties.elements_Add_Below [in Coq.MSets.MSetProperties]
OrdProperties.elements_Add_Above [in Coq.MSets.MSetProperties]
OrdProperties.elements_Add [in Coq.MSets.MSetProperties]
OrdProperties.elements_split [in Coq.MSets.MSetProperties]
OrdProperties.elements_Equal_eqlistA [in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Above [in Coq.FSets.FMapFacts]
OrdProperties.elements_Add [in Coq.FSets.FMapFacts]
OrdProperties.elements_split [in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [in Coq.FSets.FSetProperties]
OrdProperties.elements_Add_Above [in Coq.FSets.FSetProperties]
OrdProperties.elements_Add [in Coq.FSets.FSetProperties]
OrdProperties.elements_split [in Coq.FSets.FSetProperties]
OrdProperties.fold_equal [in Coq.MSets.MSetProperties]
OrdProperties.fold_4 [in Coq.MSets.MSetProperties]
OrdProperties.fold_3 [in Coq.MSets.MSetProperties]
OrdProperties.fold_Add_Below [in Coq.FSets.FMapFacts]
OrdProperties.fold_Add_Above [in Coq.FSets.FMapFacts]
OrdProperties.fold_Equal [in Coq.FSets.FMapFacts]
OrdProperties.fold_equal [in Coq.FSets.FSetProperties]
OrdProperties.fold_4 [in Coq.FSets.FSetProperties]
OrdProperties.fold_3 [in Coq.FSets.FSetProperties]
OrdProperties.gtb_1 [in Coq.MSets.MSetProperties]
OrdProperties.gtb_compat [in Coq.FSets.FMapFacts]
OrdProperties.gtb_1 [in Coq.FSets.FMapFacts]
OrdProperties.gtb_compat [in Coq.FSets.FSetProperties]
OrdProperties.gtb_1 [in Coq.FSets.FSetProperties]
OrdProperties.leb_1 [in Coq.MSets.MSetProperties]
OrdProperties.leb_compat [in Coq.FSets.FMapFacts]
OrdProperties.leb_1 [in Coq.FSets.FMapFacts]
OrdProperties.leb_compat [in Coq.FSets.FSetProperties]
OrdProperties.leb_1 [in Coq.FSets.FSetProperties]
OrdProperties.map_induction_min [in Coq.FSets.FMapFacts]
OrdProperties.map_induction_max [in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Empty [in Coq.FSets.FMapFacts]
OrdProperties.max_elt_MapsTo [in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Above [in Coq.FSets.FMapFacts]
OrdProperties.min_elt_Empty [in Coq.FSets.FMapFacts]
OrdProperties.min_elt_MapsTo [in Coq.FSets.FMapFacts]
OrdProperties.min_elt_Below [in Coq.FSets.FMapFacts]
OrdProperties.remove_fold_2 [in Coq.MSets.MSetProperties]
OrdProperties.remove_fold_2 [in Coq.FSets.FSetProperties]
OrdProperties.set_induction_min [in Coq.MSets.MSetProperties]
OrdProperties.set_induction_max [in Coq.MSets.MSetProperties]
OrdProperties.set_induction_min [in Coq.FSets.FSetProperties]
OrdProperties.set_induction_max [in Coq.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [in Coq.MSets.MSetProperties]
OrdProperties.sort_equivlistA_eqlistA [in Coq.FSets.FMapFacts]
OrdProperties.sort_equivlistA_eqlistA [in Coq.FSets.FSetProperties]
orFb [in Coq.ssr.ssrbool]
orKb [in Coq.ssr.ssrbool]
orNb [in Coq.ssr.ssrbool]
orP [in Coq.ssr.ssrbool]
orTb [in Coq.ssr.ssrbool]
or_not_r_iff_2 [in Coq.Logic.Decidable]
or_not_r_iff_1 [in Coq.Logic.Decidable]
or_not_l_iff_2 [in Coq.Logic.Decidable]
or_not_l_iff_1 [in Coq.Logic.Decidable]
or_morph [in Coq.micromega.ZifyClasses]
or_not_and [in Coq.Logic.Classical_Prop]
or_to_imply [in Coq.Logic.Classical_Prop]
or_assoc [in Coq.Init.Logic]
or_comm [in Coq.Init.Logic]
or_cancel_r [in Coq.Init.Logic]
or_cancel_l [in Coq.Init.Logic]
or_iff_compat_r [in Coq.Init.Logic]
or_iff_compat_l [in Coq.Init.Logic]
or_cnf_opt_correct [in Coq.micromega.Tauto]
or_cnf_correct [in Coq.micromega.Tauto]
or_clause_cnf_correct [in Coq.micromega.Tauto]
or_clause_correct [in Coq.micromega.Tauto]
or_cnf_opt_cnf_ff_r [in Coq.micromega.Tauto]
or_cnf_opt_cnf_ff [in Coq.micromega.Tauto]
or3P [in Coq.ssr.ssrbool]
or4P [in Coq.ssr.ssrbool]
OTF_to_TTLB.leb_trans [in Coq.Structures.Orders]
OTF_to_TTLB.leb_total [in Coq.Structures.Orders]
OTF_to_TTLB.leb_le [in Coq.Structures.Orders]
OTF_LtIsTotal.lt_total [in Coq.Structures.Orders]
OT_to_Full.le_lteq [in Coq.Structures.Orders]
OT_to_Alt.compare_trans [in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Gt [in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Lt [in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Eq [in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_sym [in Coq.Structures.OrdersAlt]
OT_from_Alt.compare_spec [in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_lt [in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_eq [in Coq.Structures.OrdersAlt]
O_S [in Coq.Init.Peano]
O_or_S [in Coq.Arith.Peano_dec]
| 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 | (68863 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 | (985 entries) |
| Binder 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 | (44709 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 | (761 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 | (1497 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 | (570 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 | (11380 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 | (976 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 | (603 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 | (298 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 | (460 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 | (476 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 | (811 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 | (1157 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 | (4018 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 | (162 entries) |