| 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) | 
D (projection)
dbody [in MetaRocq.Common.BasicAst]dbody [in MetaRocq.Erasure.EAst]
dearging_config [in MetaRocq.ErasurePlugin.Erasure]
debug [in MetaRocq.Quotation.CommonUtils]
decl_type [in MetaRocq.Common.BasicAst]
decl_body [in MetaRocq.Common.BasicAst]
decl_name [in MetaRocq.Common.BasicAst]
decl_body [in MetaRocq.Erasure.EAst]
decl_name [in MetaRocq.Erasure.EAst]
definition_entry_opaque [in MetaRocq.PCUIC.PCUICAst]
definition_entry_universes [in MetaRocq.PCUIC.PCUICAst]
definition_entry_body [in MetaRocq.PCUIC.PCUICAst]
definition_entry_type [in MetaRocq.PCUIC.PCUICAst]
definition_entry_opaque [in MetaRocq.Erasure.EAst]
definition_entry_body [in MetaRocq.Erasure.EAst]
definition_entry_opaque [in MetaRocq.Template.Ast]
definition_entry_universes [in MetaRocq.Template.Ast]
definition_entry_body [in MetaRocq.Template.Ast]
definition_entry_type [in MetaRocq.Template.Ast]
dname [in MetaRocq.Common.BasicAst]
dname [in MetaRocq.Erasure.EAst]
do_trim_ctor_masks [in MetaRocq.ErasurePlugin.ETransform]
do_trim_const_masks [in MetaRocq.ErasurePlugin.ETransform]
dtype [in MetaRocq.Common.BasicAst]