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 (72745 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 (1016 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 (47313 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 (784 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 (1547 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 (583 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 (11764 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 (959 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 (627 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 (308 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 (475 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 (492 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 (903 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 (1448 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 (4360 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 (166 entries)

O (definition)

ocancel [in Coq.ssr.ssrfun]
ocons [in Coq.micromega.Tauto]
odd [in Coq.Init.Nat]
odd_S2n_stt [in Coq.Arith.Div2]
odd_double_stt [in Coq.Arith.Div2]
odd_div2_stt [in Coq.Arith.Div2]
odd_mult_inv_r_stt [in Coq.Arith.Even]
odd_mult_inv_l_stt [in Coq.Arith.Even]
odd_mult_stt [in Coq.Arith.Even]
odd_plus_odd_inv_r_stt [in Coq.Arith.Even]
odd_plus_odd_inv_l_stt [in Coq.Arith.Even]
odd_plus_even_inv_r_stt [in Coq.Arith.Even]
odd_plus_even_inv_l_stt [in Coq.Arith.Even]
odd_even_plus_stt [in Coq.Arith.Even]
odd_plus_r_stt [in Coq.Arith.Even]
odd_plus_l_stt [in Coq.Arith.Even]
odd_plus_split_stt [in Coq.Arith.Even]
odd_even_lem_stt [in Coq.Arith.Mult]
of_pos [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
of_bits [in Coq.Init.Byte]
of_list [in Coq.Numbers.DecimalFacts]
of_nat_0 [in Coq.Strings.OctalString]
of_Z_m1 [in Coq.Strings.OctalString]
of_Z_0 [in Coq.Strings.OctalString]
of_N_0 [in Coq.Strings.OctalString]
of_pos_8 [in Coq.Strings.OctalString]
of_pos_7 [in Coq.Strings.OctalString]
of_pos_3 [in Coq.Strings.OctalString]
of_pos_2 [in Coq.Strings.OctalString]
of_pos_1 [in Coq.Strings.OctalString]
of_nat [in Coq.Strings.OctalString]
of_Z [in Coq.Strings.OctalString]
of_N [in Coq.Strings.OctalString]
of_pos [in Coq.Strings.OctalString]
of_nat_0 [in Coq.Strings.HexString]
of_Z_m1 [in Coq.Strings.HexString]
of_Z_0 [in Coq.Strings.HexString]
of_N_0 [in Coq.Strings.HexString]
of_pos_16 [in Coq.Strings.HexString]
of_pos_15 [in Coq.Strings.HexString]
of_pos_14 [in Coq.Strings.HexString]
of_pos_13 [in Coq.Strings.HexString]
of_pos_12 [in Coq.Strings.HexString]
of_pos_11 [in Coq.Strings.HexString]
of_pos_10 [in Coq.Strings.HexString]
of_pos_9 [in Coq.Strings.HexString]
of_pos_8 [in Coq.Strings.HexString]
of_pos_7 [in Coq.Strings.HexString]
of_pos_3 [in Coq.Strings.HexString]
of_pos_2 [in Coq.Strings.HexString]
of_pos_1 [in Coq.Strings.HexString]
of_nat [in Coq.Strings.HexString]
of_Z [in Coq.Strings.HexString]
of_N [in Coq.Strings.HexString]
of_pos [in Coq.Strings.HexString]
of_num_int [in Coq.Init.Nat]
of_hex_int [in Coq.Init.Nat]
of_int [in Coq.Init.Nat]
of_num_uint [in Coq.Init.Nat]
of_hex_uint [in Coq.Init.Nat]
of_hex_uint_acc [in Coq.Init.Nat]
of_uint [in Coq.Init.Nat]
of_uint_acc [in Coq.Init.Nat]
of_nat [in Coq.Arith.Cantor]
of_void [in Coq.ssr.ssrfun]
of_number [in Coq.Reals.Rdefinitions]
of_hexadecimal [in Coq.Reals.Rdefinitions]
of_decimal [in Coq.Reals.Rdefinitions]
of_list [in Coq.Numbers.HexadecimalFacts]
of_nat_0 [in Coq.Strings.BinaryString]
of_Z_m1 [in Coq.Strings.BinaryString]
of_Z_0 [in Coq.Strings.BinaryString]
of_N_0 [in Coq.Strings.BinaryString]
of_pos_3 [in Coq.Strings.BinaryString]
of_pos_2 [in Coq.Strings.BinaryString]
of_pos_1 [in Coq.Strings.BinaryString]
of_nat [in Coq.Strings.BinaryString]
of_Z [in Coq.Strings.BinaryString]
of_N [in Coq.Strings.BinaryString]
of_pos [in Coq.Strings.BinaryString]
of_nat_lt [in Coq.Vectors.Fin]
of_nat [in Coq.Vectors.Fin]
of_N [in Coq.Strings.Byte]
of_nat [in Coq.Strings.Byte]
of_Z [in Coq.Numbers.Cyclic.Int63.Uint63]
of_pos [in Coq.Numbers.Cyclic.Int63.Uint63]
of_pos_rec [in Coq.Numbers.Cyclic.Int63.Uint63]
of_list [in Coq.Vectors.VectorDef]
of_Bvector [in Coq.Strings.ByteVector]
of_string [in Coq.Strings.ByteVector]
of_number [in Coq.QArith.QArith_base]
of_hexadecimal [in Coq.QArith.QArith_base]
of_decimal [in Coq.QArith.QArith_base]
OmniscientFunctionalChoice_on [in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice_on [in Coq.Logic.ChoiceFacts]
On [in Coq.Numbers.Cyclic.Int31.Int31]
one [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
one [in Coq.Floats.PrimFloat]
one [in Coq.Init.Nat]
one [in Coq.Strings.Ascii]
onPhantom [in Coq.ssr.ssrbool]
OpAdd [in Coq.micromega.RingMicromega]
open_set [in Coq.Reals.Rtopology]
open_interval [in Coq.Reals.RiemannInt_SF]
OpMult [in Coq.micromega.RingMicromega]
opp [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp [in Coq.Init.Decimal]
opp [in Coq.Init.Hexadecimal]
opp [in Coq.Numbers.Cyclic.Int63.Uint63]
oppc [in Coq.Numbers.Cyclic.Int63.Uint63]
oppcarry [in Coq.Numbers.Cyclic.Int63.Uint63]
opp_carry [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_c [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_fct [in Coq.Reals.Ranalysis1]
opp_seq [in Coq.Reals.SeqProp]
opp31 [in Coq.Numbers.Cyclic.Int31.Int31]
Ops.add [in Coq.MSets.MSetWeakList]
Ops.add [in Coq.MSets.MSetList]
Ops.add [in Coq.MSets.MSetAVL]
Ops.add [in Coq.MSets.MSetRBT]
Ops.append [in Coq.MSets.MSetRBT]
Ops.assert_false [in Coq.MSets.MSetAVL]
Ops.bal [in Coq.MSets.MSetAVL]
Ops.bogus [in Coq.MSets.MSetRBT]
Ops.cardinal [in Coq.MSets.MSetWeakList]
Ops.cardinal [in Coq.MSets.MSetList]
Ops.cardinal [in Coq.MSets.MSetGenTree]
Ops.choose [in Coq.MSets.MSetWeakList]
Ops.choose [in Coq.MSets.MSetList]
Ops.choose [in Coq.MSets.MSetGenTree]
Ops.compare [in Coq.MSets.MSetList]
Ops.compare [in Coq.MSets.MSetGenTree]
Ops.compare_height [in Coq.MSets.MSetRBT]
Ops.compare_end [in Coq.MSets.MSetGenTree]
Ops.compare_cont [in Coq.MSets.MSetGenTree]
Ops.compare_more [in Coq.MSets.MSetGenTree]
Ops.concat [in Coq.MSets.MSetAVL]
Ops.cons [in Coq.MSets.MSetGenTree]
Ops.create [in Coq.MSets.MSetAVL]
Ops.del [in Coq.MSets.MSetRBT]
Ops.delmin [in Coq.MSets.MSetRBT]
Ops.diff [in Coq.MSets.MSetWeakList]
Ops.diff [in Coq.MSets.MSetList]
Ops.diff [in Coq.MSets.MSetAVL]
Ops.diff [in Coq.MSets.MSetRBT]
Ops.diff_list [in Coq.MSets.MSetRBT]
Ops.elements [in Coq.MSets.MSetWeakList]
Ops.elements [in Coq.MSets.MSetList]
Ops.elements [in Coq.MSets.MSetGenTree]
Ops.elements_aux [in Coq.MSets.MSetGenTree]
Ops.elt [in Coq.MSets.MSetWeakList]
Ops.elt [in Coq.MSets.MSetList]
Ops.elt [in Coq.MSets.MSetGenTree]
Ops.empty [in Coq.MSets.MSetWeakList]
Ops.empty [in Coq.MSets.MSetList]
Ops.empty [in Coq.MSets.MSetGenTree]
Ops.equal [in Coq.MSets.MSetWeakList]
Ops.equal [in Coq.MSets.MSetList]
Ops.equal [in Coq.MSets.MSetGenTree]
Ops.exists_ [in Coq.MSets.MSetWeakList]
Ops.exists_ [in Coq.MSets.MSetList]
Ops.exists_ [in Coq.MSets.MSetGenTree]
Ops.filter [in Coq.MSets.MSetWeakList]
Ops.filter [in Coq.MSets.MSetList]
Ops.filter [in Coq.MSets.MSetAVL]
Ops.filter [in Coq.MSets.MSetRBT]
Ops.filter_aux [in Coq.MSets.MSetRBT]
Ops.fold [in Coq.MSets.MSetWeakList]
Ops.fold [in Coq.MSets.MSetList]
Ops.fold [in Coq.MSets.MSetGenTree]
Ops.for_all [in Coq.MSets.MSetWeakList]
Ops.for_all [in Coq.MSets.MSetList]
Ops.for_all [in Coq.MSets.MSetGenTree]
Ops.height [in Coq.MSets.MSetAVL]
Ops.ins [in Coq.MSets.MSetRBT]
Ops.inter [in Coq.MSets.MSetWeakList]
Ops.inter [in Coq.MSets.MSetList]
Ops.inter [in Coq.MSets.MSetAVL]
Ops.inter [in Coq.MSets.MSetRBT]
Ops.inter_list [in Coq.MSets.MSetRBT]
Ops.is_empty [in Coq.MSets.MSetWeakList]
Ops.is_empty [in Coq.MSets.MSetList]
Ops.is_empty [in Coq.MSets.MSetGenTree]
Ops.join [in Coq.MSets.MSetAVL]
Ops.lbal [in Coq.MSets.MSetRBT]
Ops.lbalS [in Coq.MSets.MSetRBT]
Ops.linear_diff [in Coq.MSets.MSetRBT]
Ops.linear_inter [in Coq.MSets.MSetRBT]
Ops.linear_union [in Coq.MSets.MSetRBT]
Ops.makeBlack [in Coq.MSets.MSetRBT]
Ops.makeRed [in Coq.MSets.MSetRBT]
Ops.maxdepth [in Coq.MSets.MSetGenTree]
Ops.max_elt [in Coq.MSets.MSetList]
Ops.max_elt [in Coq.MSets.MSetGenTree]
Ops.mem [in Coq.MSets.MSetWeakList]
Ops.mem [in Coq.MSets.MSetList]
Ops.mem [in Coq.MSets.MSetGenTree]
Ops.merge [in Coq.MSets.MSetAVL]
Ops.mindepth [in Coq.MSets.MSetGenTree]
Ops.min_elt [in Coq.MSets.MSetList]
Ops.min_elt [in Coq.MSets.MSetGenTree]
Ops.partition [in Coq.MSets.MSetWeakList]
Ops.partition [in Coq.MSets.MSetList]
Ops.partition [in Coq.MSets.MSetAVL]
Ops.partition [in Coq.MSets.MSetRBT]
Ops.partition_aux [in Coq.MSets.MSetRBT]
Ops.plength [in Coq.MSets.MSetRBT]
Ops.plength_aux [in Coq.MSets.MSetRBT]
Ops.rbal [in Coq.MSets.MSetRBT]
Ops.rbalS [in Coq.MSets.MSetRBT]
Ops.rbal' [in Coq.MSets.MSetRBT]
Ops.remove [in Coq.MSets.MSetWeakList]
Ops.remove [in Coq.MSets.MSetList]
Ops.remove [in Coq.MSets.MSetAVL]
Ops.remove [in Coq.MSets.MSetRBT]
Ops.remove_min [in Coq.MSets.MSetAVL]
Ops.remove_min [in Coq.MSets.MSetRBT]
Ops.rev_elements [in Coq.MSets.MSetGenTree]
Ops.rev_elements_aux [in Coq.MSets.MSetGenTree]
Ops.singleton [in Coq.MSets.MSetWeakList]
Ops.singleton [in Coq.MSets.MSetList]
Ops.singleton [in Coq.MSets.MSetAVL]
Ops.singleton [in Coq.MSets.MSetRBT]
Ops.skip_black [in Coq.MSets.MSetRBT]
Ops.skip_red [in Coq.MSets.MSetRBT]
Ops.split [in Coq.MSets.MSetAVL]
Ops.subset [in Coq.MSets.MSetWeakList]
Ops.subset [in Coq.MSets.MSetList]
Ops.subset [in Coq.MSets.MSetGenTree]
Ops.subsetl [in Coq.MSets.MSetGenTree]
Ops.subsetr [in Coq.MSets.MSetGenTree]
Ops.t [in Coq.MSets.MSetWeakList]
Ops.t [in Coq.MSets.MSetList]
Ops.t [in Coq.MSets.MSetAVL]
Ops.t [in Coq.MSets.MSetRBT]
Ops.treeify [in Coq.MSets.MSetRBT]
Ops.treeify_aux [in Coq.MSets.MSetRBT]
Ops.treeify_cont [in Coq.MSets.MSetRBT]
Ops.treeify_one [in Coq.MSets.MSetRBT]
Ops.treeify_zero [in Coq.MSets.MSetRBT]
Ops.union [in Coq.MSets.MSetWeakList]
Ops.union [in Coq.MSets.MSetList]
Ops.union [in Coq.MSets.MSetAVL]
Ops.union [in Coq.MSets.MSetRBT]
Ops.union_list [in Coq.MSets.MSetRBT]
option_map [in Coq.Init.Datatypes]
Option.apply [in Coq.ssr.ssrfun]
Option.bind [in Coq.ssr.ssrfun]
Option.default [in Coq.ssr.ssrfun]
Option.map [in Coq.ssr.ssrfun]
orb [in Coq.Init.Datatypes]
OrderedTypeFacts.eqb [in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_dec [in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_dec [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_trans [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_sym [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_refl [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.IsTO.eq_equiv [in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_total [in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_compat [in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_strorder [in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_irrefl [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.lt_trans [in Coq.Structures.OrdersFacts]
OrderedTypeFacts.TO.eq [in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.le [in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.lt [in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.t [in Coq.Structures.OrderedType]
OrderedTypeRev.compare [in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq [in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq_dec [in Coq.Structures.OrdersFacts]
OrderedTypeRev.le [in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt [in Coq.Structures.OrdersFacts]
OrderedTypeRev.t [in Coq.Structures.OrdersFacts]
OrderedType_to_Alt.compare [in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.t [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_dec [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.compare [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_trans [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_trans [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq [in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.t [in Coq.Structures.OrderedTypeAlt]
ordered_Rlist [in Coq.Reals.RList]
OrderFacts.eq_le [in Coq.Structures.OrdersTac]
OrderFacts.eq_lt [in Coq.Structures.OrdersTac]
OrderFacts.eq_trans [in Coq.Structures.OrdersTac]
OrderFacts.interp_ord [in Coq.Structures.OrdersTac]
OrderFacts.le_eq [in Coq.Structures.OrdersTac]
OrderFacts.le_lt_trans [in Coq.Structures.OrdersTac]
OrderFacts.le_trans [in Coq.Structures.OrdersTac]
OrderFacts.lt_eq [in Coq.Structures.OrdersTac]
OrderFacts.lt_le_trans [in Coq.Structures.OrdersTac]
OrderFacts.lt_trans [in Coq.Structures.OrdersTac]
OrdProperties.Above [in Coq.MSets.MSetProperties]
OrdProperties.Above [in Coq.FSets.FMapFacts]
OrdProperties.Above [in Coq.FSets.FSetProperties]
OrdProperties.Below [in Coq.MSets.MSetProperties]
OrdProperties.Below [in Coq.FSets.FMapFacts]
OrdProperties.Below [in Coq.FSets.FSetProperties]
OrdProperties.elements_ge [in Coq.MSets.MSetProperties]
OrdProperties.elements_lt [in Coq.MSets.MSetProperties]
OrdProperties.elements_ge [in Coq.FSets.FMapFacts]
OrdProperties.elements_lt [in Coq.FSets.FMapFacts]
OrdProperties.elements_ge [in Coq.FSets.FSetProperties]
OrdProperties.elements_lt [in Coq.FSets.FSetProperties]
OrdProperties.gtb [in Coq.MSets.MSetProperties]
OrdProperties.gtb [in Coq.FSets.FMapFacts]
OrdProperties.gtb [in Coq.FSets.FSetProperties]
OrdProperties.leb [in Coq.MSets.MSetProperties]
OrdProperties.leb [in Coq.FSets.FMapFacts]
OrdProperties.leb [in Coq.FSets.FSetProperties]
OrdProperties.max_elt [in Coq.FSets.FMapFacts]
OrdProperties.max_elt_aux [in Coq.FSets.FMapFacts]
OrdProperties.min_elt [in Coq.FSets.FMapFacts]
or_indd [in Coq.Logic.ClassicalFacts]
or_elim_redr [in Coq.Logic.ClassicalFacts]
or_elim_redl [in Coq.Logic.ClassicalFacts]
or_is_X [in Coq.micromega.Tauto]
or_cnf_opt [in Coq.micromega.Tauto]
or_cnf [in Coq.micromega.Tauto]
or_clause_cnf [in Coq.micromega.Tauto]
or_clause [in Coq.micromega.Tauto]
OTF_to_TTLB.t [in Coq.Structures.Orders]
OTF_to_TTLB.leb [in Coq.Structures.Orders]
OT_to_Full.le [in Coq.Structures.Orders]
OT_to_Alt.compare [in Coq.Structures.OrdersAlt]
OT_to_Alt.t [in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_dec [in Coq.Structures.OrdersAlt]
OT_from_Alt.compare [in Coq.Structures.OrdersAlt]
OT_from_Alt.lt [in Coq.Structures.OrdersAlt]
OT_from_Alt.eq [in Coq.Structures.OrdersAlt]
OT_from_Alt.t [in Coq.Structures.OrdersAlt]
over [in Coq.ssr.ssreflect]
O_witness [in Coq.Logic.ConstructiveEpsilon]


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 (72745 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 (1016 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 (47313 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 (784 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 (1547 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 (583 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 (11764 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 (959 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 (627 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 (308 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 (475 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 (492 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 (903 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 (1448 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 (4360 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 (166 entries)