| 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 | (1589 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 | (10 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 | (24 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 | (137 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 | (50 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 | (26 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 | (262 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 | (184 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 | (45 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 | (37 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 | (26 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 | (19 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 | (15 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 | (742 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 | (12 entries) | 
O
obnd [definition, in VerifiedExtraction.Benchmarks.lib.vs]OCamlFFI [library]
ocons [definition, in VerifiedExtraction.Benchmarks.lib.vs]
of_string_to_string [lemma, in Malfunction.CompileCorrect]
omap [definition, in VerifiedExtraction.Benchmarks.lib.vs]
omapl [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ONE [constructor, in Top.test_extract]
ONE [constructor, in Top.Tests]
option [section, in VerifiedExtraction.Benchmarks.lib.vs]
option_def [definition, in Malfunction.SemanticsSpec]
option.A [variable, in VerifiedExtraction.Benchmarks.lib.vs]
option.B [variable, in VerifiedExtraction.Benchmarks.lib.vs]
option.f [variable, in VerifiedExtraction.Benchmarks.lib.vs]
option.h [variable, in VerifiedExtraction.Benchmarks.lib.vs]
option.o [variable, in VerifiedExtraction.Benchmarks.lib.vs]
Or [constructor, in Malfunction.Malfunction]
OrderedClause [module, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.compare [definition, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.compare_spec [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.eq [definition, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.eq_dec [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.eq_equiv [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.lt [definition, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.lt_strorder [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.lt_compat [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
OrderedClause.t [definition, in VerifiedExtraction.Benchmarks.lib.vs]
order_eqv_pure_atoms [definition, in VerifiedExtraction.Benchmarks.lib.vs]
order_eqv_clause [definition, in VerifiedExtraction.Benchmarks.lib.vs]
order_eqv_pure_atom [definition, in VerifiedExtraction.Benchmarks.lib.vs]