| 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 | (18986 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 | (228 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 | (297 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 | (1273 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 | (313 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 | (8135 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 | (1490 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 | (52 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |
B (lemma)
banon_list [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]banon_eq_binder_annot [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
banon_spec [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
bbody_branch_depth [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
bcontext_trans_length [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
bd_wf_local_rel [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
bd_wf_local [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
bidirectional_renaming [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
bidirectional_on_free_vars [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
bidirectional_unique [in MetaRocq.PCUIC.Bidirectional.BDUnique]
bidirectional_to_pcuic [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
bidirectional_from_pcuic [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
bidir_ind_env [in MetaRocq.PCUIC.Bidirectional.BDTyping]
biimpl_introT [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
binder_anonymize [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
bool_pirr [in MetaRocq.PCUIC.Syntax.PCUICViews]
branch_helper [in MetaRocq.SafeChecker.PCUICTypeChecker]
br_fvs_pres [in MetaRocq.PCUIC.PCUICNormal]
build_wf_env_from_env_eq [in MetaRocq.ErasurePlugin.ETransform]