Library Malfunction.Examples.fail-big.fail

From VerifiedExtraction Require Import Extraction.

Inductive big : Set :=
|C0
|C1 (o : big)
|C2 (o : big)
|C3 (o : big)
|C4 (o : big)
|C5 (o : big)
|C6 (o : big)
|C7 (o : big)
|C8 (o : big)
|C9 (o : big)
|C10 (o : big)
|C11 (o : big)
|C12 (o : big)
|C13 (o : big)
|C14 (o : big)
|C15 (o : big)
|C16 (o : big)
|C17 (o : big)
|C18 (o : big)
|C19 (o : big)
|C20 (o : big)
|C21 (o : big)
|C22 (o : big)
|C23 (o : big)
|C24 (o : big)
|C25 (o : big)
|C26 (o : big)
|C27 (o : big)
|C28 (o : big)
|C29 (o : big)
|C30 (o : big)
|C31 (o : big)
|C32 (o : big)
|C33 (o : big)
|C34 (o : big)
|C35 (o : big)
|C36 (o : big)
|C37 (o : big)
|C38 (o : big)
|C39 (o : big)
|C40 (o : big)
|C41 (o : big)
|C42 (o : big)
|C43 (o : big)
|C44 (o : big)
|C45 (o : big)
|C46 (o : big)
|C47 (o : big)
|C48 (o : big)
|C49 (o : big)
|C50 (o : big)
|C51 (o : big)
|C52 (o : big)
|C53 (o : big)
|C54 (o : big)
|C55 (o : big)
|C56 (o : big)
|C57 (o : big)
|C58 (o : big)
|C59 (o : big)
|C60 (o : big)
|C61 (o : big)
|C62 (o : big)
|C63 (o : big)
|C64 (o : big)
|C65 (o : big)
|C66 (o : big)
|C67 (o : big)
|C68 (o : big)
|C69 (o : big)
|C70 (o : big)
|C71 (o : big)
|C72 (o : big)
|C73 (o : big)
|C74 (o : big)
|C75 (o : big)
|C76 (o : big)
|C77 (o : big)
|C78 (o : big)
|C79 (o : big)
|C80 (o : big)
|C81 (o : big)
|C82 (o : big)
|C83 (o : big)
|C84 (o : big)
|C85 (o : big)
|C86 (o : big)
|C87 (o : big)
|C88 (o : big)
|C89 (o : big)
|C90 (o : big)
|C91 (o : big)
|C92 (o : big)
|C93 (o : big)
|C94 (o : big)
|C95 (o : big)
|C96 (o : big)
|C97 (o : big)
|C98 (o : big)
|C99 (o : big)
|C100 (o : big)
|C101 (o : big)
|C102 (o : big)
|C103 (o : big)
|C104 (o : big)
|C105 (o : big)
|C106 (o : big)
|C107 (o : big)
|C108 (o : big)
|C109 (o : big)
|C110 (o : big)
|C111 (o : big)
|C112 (o : big)
|C113 (o : big)
|C114 (o : big)
|C115 (o : big)
|C116 (o : big)
|C117 (o : big)
|C118 (o : big)
|C119 (o : big)
|C120 (o : big)
|C121 (o : big)
|C122 (o : big)
|C123 (o : big)
|C124 (o : big)
|C125 (o : big)
|C126 (o : big)
|C127 (o : big)
|C128 (o : big)
|C129 (o : big)
|C130 (o : big)
|C131 (o : big)
|C132 (o : big)
|C133 (o : big)
|C134 (o : big)
|C135 (o : big)
|C136 (o : big)
|C137 (o : big)
|C138 (o : big)
|C139 (o : big)
|C140 (o : big)
|C141 (o : big)
|C142 (o : big)
|C143 (o : big)
|C144 (o : big)
|C145 (o : big)
|C146 (o : big)
|C147 (o : big)
|C148 (o : big)
|C149 (o : big)
|C150 (o : big)
|C151 (o : big)
|C152 (o : big)
|C153 (o : big)
|C154 (o : big)
|C155 (o : big)
|C156 (o : big)
|C157 (o : big)
|C158 (o : big)
|C159 (o : big)
|C160 (o : big)
|C161 (o : big)
|C162 (o : big)
|C163 (o : big)
|C164 (o : big)
|C165 (o : big)
|C166 (o : big)
|C167 (o : big)
|C168 (o : big)
|C169 (o : big)
|C170 (o : big)
|C171 (o : big)
|C172 (o : big)
|C173 (o : big)
|C174 (o : big)
|C175 (o : big)
|C176 (o : big)
|C177 (o : big)
|C178 (o : big)
|C179 (o : big)
|C180 (o : big)
|C181 (o : big)
|C182 (o : big)
|C183 (o : big)
|C184 (o : big)
|C185 (o : big)
|C186 (o : big)
|C187 (o : big)
|C188 (o : big)
|C189 (o : big)
|C190 (o : big)
|C191 (o : big)
|C192 (o : big)
|C193 (o : big)
|C194 (o : big)
|C195 (o : big)
|C196 (o : big)
|C197 (o : big)
|C198 (o : big)
|C199 (o : big)
|C200 (o : big)
|C201 (o : big)
|C202 (o : big).

Definition id (o : big) := o.

Fail Verified Extraction C202.