| 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) |
C
c [definition, in VerifiedExtraction.Benchmarks.lib.vs]camlType [inductive, in Malfunction.RealizabilitySemantics]
camlType_rect [definition, in Malfunction.RealizabilitySemantics]
camlValue_to_RocqValue [lemma, in Malfunction.Firstorder]
CanonicalHeap [definition, in Malfunction.Interpreter]
CanonicalHeap [definition, in Malfunction.SemanticsSpec]
CanonicalPointer [definition, in Malfunction.SemanticsSpec]
canons [abbreviation, in VerifiedExtraction.Benchmarks.lib.vs]
capitalize [definition, in Malfunction.PrintMli]
capitalize_char [definition, in Malfunction.PrintMli]
cardinal_map [lemma, in VerifiedExtraction.Benchmarks.lib.Color]
carry [definition, in VerifiedExtraction.Benchmarks.lib.Binom]
case [inductive, in Malfunction.Malfunction]
case_sind [definition, in Malfunction.Malfunction]
case_rec [definition, in Malfunction.Malfunction]
case_ind [definition, in Malfunction.Malfunction]
case_rect [definition, in Malfunction.Malfunction]
cclose [definition, in VerifiedExtraction.Benchmarks.lib.vs]
cclose_aux [definition, in VerifiedExtraction.Benchmarks.lib.vs]
cclosure [section, in VerifiedExtraction.Benchmarks.lib.vs]
cclosure.A [variable, in VerifiedExtraction.Benchmarks.lib.vs]
cclosure.A_cmp [variable, in VerifiedExtraction.Benchmarks.lib.vs]
cclosure.B [variable, in VerifiedExtraction.Benchmarks.lib.vs]
cclosure.B_cmp [variable, in VerifiedExtraction.Benchmarks.lib.vs]
cclosure.fAB [variable, in VerifiedExtraction.Benchmarks.lib.vs]
CexpEf [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
CexpL [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
CexpR [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
ce_harder_ent3 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_harder_ent2 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_harder_ent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_example_ent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_example2_myfail [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_example1_myfail [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_example2_myent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_example1_myent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_example_myent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_type_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_type_rec [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_type_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_type_rect [definition, in VerifiedExtraction.Benchmarks.lib.vs]
ce_type [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
cf_ [instance, in Malfunction.Firstorder]
char63_to_byte [definition, in Malfunction.Compile]
check_lt [definition, in Top.test_extraction_malfunction]
check_good_for_extraction [definition, in Malfunction.Pipeline]
check_good_for_extraction_rec [definition, in Malfunction.Pipeline]
clause [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
clause_list2set [definition, in VerifiedExtraction.Benchmarks.lib.vs]
clause_length [definition, in VerifiedExtraction.Benchmarks.lib.vs]
clause_cspec' [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
clause_prio [definition, in VerifiedExtraction.Benchmarks.lib.vs]
clause_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
clause_rec [definition, in VerifiedExtraction.Benchmarks.lib.vs]
clause_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
clause_rect [definition, in VerifiedExtraction.Benchmarks.lib.vs]
closed_decls_closed_ctx [lemma, in Malfunction.Firstorder]
closed_firstorder_type [lemma, in Malfunction.Firstorder]
cnf [definition, in VerifiedExtraction.Benchmarks.lib.vs]
CoInd [module, in Top.tutorial]
coind [library]
CoInd.head [projection, in Top.tutorial]
CoInd.ones [definition, in Top.tutorial]
CoInd.stream [record, in Top.tutorial]
CoInd.tail [projection, in Top.tutorial]
CoInd.take [definition, in Top.tutorial]
CoInd.test_ones [definition, in Top.tutorial]
color [definition, in VerifiedExtraction.Benchmarks.lib.Color]
Color [library]
coloring [definition, in VerifiedExtraction.Benchmarks.lib.Color]
coloring_ok [definition, in VerifiedExtraction.Benchmarks.lib.Color]
colors_of [definition, in VerifiedExtraction.Benchmarks.lib.Color]
color_correct [lemma, in VerifiedExtraction.Benchmarks.lib.Color]
color1 [definition, in VerifiedExtraction.Benchmarks.lib.Color]
comp [section, in VerifiedExtraction.Benchmarks.lib.vs]
compare_clause2 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
compare_clause'1 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
compare_clause_length [definition, in VerifiedExtraction.Benchmarks.lib.vs]
compare_clause' [definition, in VerifiedExtraction.Benchmarks.lib.vs]
compare_clause [definition, in VerifiedExtraction.Benchmarks.lib.vs]
compare_space_atom [definition, in VerifiedExtraction.Benchmarks.lib.vs]
compare_list_pure_atom_cmp_rfl [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
compare_list [definition, in VerifiedExtraction.Benchmarks.lib.vs]
comparison_eqb [definition, in Malfunction.SemanticsSpec]
CompatibleHeap [record, in Malfunction.RealizabilitySemantics]
CompatibleHeap [record, in Malfunction.Interpreter]
CompatiblePtr [record, in Malfunction.Interpreter]
CompatiblePtr_sym [definition, in Malfunction.Interpreter]
compcert [library]
compile [definition, in Malfunction.Compile]
Compile [section, in Malfunction.Compile]
Compile [library]
CompileCorrect [library]
compile_compose [lemma, in Malfunction.Firstorder]
compile_malfunction_pipeline_eq [lemma, in Malfunction.Firstorder]
compile_pipeline_eq [lemma, in Malfunction.Firstorder]
compile_pipeline_tConstruct_cons [definition, in Malfunction.Firstorder]
compile_pipeline_tConstruct_nil [lemma, in Malfunction.Firstorder]
compile_function [lemma, in Malfunction.Firstorder]
compile_value_pure [lemma, in Malfunction.Firstorder]
compile_pure [lemma, in Malfunction.Firstorder]
compile_pipeline [definition, in Malfunction.Firstorder]
compile_malfunction [definition, in Malfunction.Pipeline]
compile_malfunction_gen [definition, in Malfunction.Pipeline]
compile_malfunction_pipeline [definition, in Malfunction.Pipeline]
compile_malfunction_pipeline.Normalisation [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.typing [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.expt [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.expΣ [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.HΣ [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.T [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.t [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.Σ [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.HH [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline.HP [variable, in Malfunction.Pipeline]
compile_malfunction_pipeline [section, in Malfunction.Pipeline]
compile_to_malfunction [definition, in Malfunction.Pipeline]
compile_app_not_nil [lemma, in Malfunction.CompileCorrect]
compile_extends [lemma, in Malfunction.CompileCorrect]
compile_wellformed [lemma, in Malfunction.CompileCorrect]
compile_correct [lemma, in Malfunction.CompileCorrect]
compile_value [definition, in Malfunction.CompileCorrect]
compile_program [definition, in Malfunction.Compile]
compile_env [definition, in Malfunction.Compile]
compile_constant_decl [definition, in Malfunction.Compile]
compile_array [definition, in Malfunction.Compile]
compile_value_mf_fo [lemma, in Malfunction.PipelineCorrect]
compile_value_mf_fo' [lemma, in Malfunction.PipelineCorrect]
compile_malfunction_pipeline_app [lemma, in Malfunction.PipelineCorrect]
compile_value_mf_eq [lemma, in Malfunction.PipelineCorrect]
compile_value_mf.compile_value_mf [variable, in Malfunction.PipelineCorrect]
compile_value_mf.Σ_t' [variable, in Malfunction.PipelineCorrect]
compile_value_mf.Σ_v [variable, in Malfunction.PipelineCorrect]
compile_value_mf.Heval [variable, in Malfunction.PipelineCorrect]
compile_value_mf.Σ_t [variable, in Malfunction.PipelineCorrect]
compile_value_mf.typing [variable, in Malfunction.PipelineCorrect]
compile_value_mf.T [variable, in Malfunction.PipelineCorrect]
compile_named_value [definition, in Malfunction.PipelineCorrect]
compile_value_eval_fo_repr [lemma, in Malfunction.PipelineCorrect]
compile_value_mf.Normalisation [variable, in Malfunction.PipelineCorrect]
compile_value_mf.noParam [variable, in Malfunction.PipelineCorrect]
compile_value_mf.fo [variable, in Malfunction.PipelineCorrect]
compile_value_mf.args [variable, in Malfunction.PipelineCorrect]
compile_value_mf.u [variable, in Malfunction.PipelineCorrect]
compile_value_mf.i [variable, in Malfunction.PipelineCorrect]
compile_value_mf.v [variable, in Malfunction.PipelineCorrect]
compile_value_mf.expt [variable, in Malfunction.PipelineCorrect]
compile_value_mf.t [variable, in Malfunction.PipelineCorrect]
compile_value_mf.expΣ [variable, in Malfunction.PipelineCorrect]
compile_value_mf.HΣ [variable, in Malfunction.PipelineCorrect]
compile_value_mf.no_axioms [variable, in Malfunction.PipelineCorrect]
compile_value_mf.Σ [variable, in Malfunction.PipelineCorrect]
compile_value_mf.HH [variable, in Malfunction.PipelineCorrect]
compile_value_mf.HP [variable, in Malfunction.PipelineCorrect]
compile_value_mf [section, in Malfunction.PipelineCorrect]
compile_value_mf' [definition, in Malfunction.PipelineCorrect]
compile_value_mf_aux [definition, in Malfunction.PipelineCorrect]
compile_value_box_mkApps [lemma, in Malfunction.PipelineCorrect]
Compile.Σ [variable, in Malfunction.Compile]
compose [definition, in VerifiedExtraction.Benchmarks.lib.vs]
CompSpec' [definition, in VerifiedExtraction.Benchmarks.lib.vs]
comp_trans [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
comp_refl [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
comp.a [variable, in VerifiedExtraction.Benchmarks.lib.vs]
comp.A [variable, in VerifiedExtraction.Benchmarks.lib.vs]
comp.B [variable, in VerifiedExtraction.Benchmarks.lib.vs]
comp.C [variable, in VerifiedExtraction.Benchmarks.lib.vs]
comp.f [variable, in VerifiedExtraction.Benchmarks.lib.vs]
comp.g [variable, in VerifiedExtraction.Benchmarks.lib.vs]
cond [definition, in Malfunction.SemanticsSpec]
cond_correct [lemma, in Malfunction.Interpreter]
Cons [definition, in Malfunction.Serialize]
con2c [abbreviation, in Malfunction.Deserialize]
coq_user_error [axiom, in Malfunction.FFI]
coq_msg_debug [axiom, in Malfunction.FFI]
coq_msg_notice [axiom, in Malfunction.FFI]
coq_msg_info [axiom, in Malfunction.FFI]
coq_false [definition, in Top.test_extract_inductive]
coq_true [definition, in Top.test_extract_inductive]
cstr_nargs [definition, in Malfunction.RealizabilitySemantics]
ctors_max_length [projection, in Malfunction.Firstorder]
C_example [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
| 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) |