# Coq Reference Manual

# Index of Error Messages

ident already exists, 1.3.1, 1.3.1, 1.3.2, 1.3.2, 1.3.5, 23.1.2 Argument of match does not evaluate to a term, 9.2 Attempt to save an incomplete proof, 7.1.2 already exists, 1.3.5 arguments of ring_simplify do not have all the same type, 24.4 Bad magic number, 6.5.1 Bound head variable, 8.9.1, 8.9.1 bad lemma for decidability of equality, 24.5 bad ring structure, 24.5 Can’t find file ident on loadpath, 6.4.1 Cannot build functional inversion principle, 2.3 Cannot define graph for ident…, 2.3 Cannot define principle(s) for ident…, 2.3 Cannot find induction information on qualid, 8.5.5 Cannot find inversion information for hypothesis ident, 8.15.1 Cannot find library foo in loadpath, 6.5.1 Cannot find the source class of qualid, 18.6.1 Cannot handle mutually (co)inductive records., 2.1 Cannot infer a term for this placeholder, 2.7.3, 8.2.3 Cannot load qualid: no physical path bound to dirpath, 6.5.1 Cannot move ident1 after ident2: it depends on ident2, 8.3.5 Cannot move ident1 after ident2: it occurs in ident2, 8.3.5 Cannot recognize class1 as a source class of qualid, 18.6.1 Cannot solve the goal, 9.2 Cannot use mutual definition with well-founded recursion or measure, 2.3 Compiled library ident.vo makes inconsistent assumptions over library qualid, 6.5.1 cannot be used as a hint, 8.9.1, 8.9.1 cannot find a declared ring structure for equality term, 24.4 cannot find a declared ring structure over term, 24.4 does not denote an evaluable constant, 8.7.5 does not respect the uniform inheritance condition, 18.6.1 Error: No such unproven subgoal, 7.2.7 Error: The term term has type type while it is expected to have type type, 1.3.2 Error: This proof is focused, but cannot be unfocused this way, 7.2.6, 7.2.7 Failed to progress, 9.2 File not found on loadpath : string, 6.5.3 Found target class class instead of class2, 18.6.1 Funclass cannot be a source class, 18.6.1 Goal is solvable by congruence but some arguments are missing. Try congruence with …, replacing metavariables by arbitrary terms., 8.10.5 goal does not satisfy the expected preconditions, 8.5.7 Hypothesis ident must contain at least one Function, 8.15.1 I couldn’t solve goal, 8.10.5 I don’t know how to handle dependent equality, 8.10.5 Impossible to unify … with …, 8.2.4 Impossible to unify … with …., 8.6.4 In environment … the term: term2 does not have type term1, 23.1.2 Invalid backtrack, 6.7.2, 6.7.3 invalid argument, 8.2.3 is used in the hypothesis, 8.3.3, 8.3.4 is already a coercion, 18.6.1 is already used, 8.3.1, 8.3.6 is not a function, 18.6.1 is not a local definition, 8.3.3 is not a module, 2.5.8 is not an inductive type, 8.9.1 is used in conclusion, 8.4.1 is used in hypothesis, 8.4.1 is used in the conclusion, 8.3.3 Loading of ML object file forbidden in a native Coq, 6.5.3 Module/section module not found, 6.3.6 must be a transparent constant, 18.6.2 No applicable tactic, 9.2 No argument name ident, 2.3 No discriminable equalities, 8.5.6 No evars, 8.12.4 No focused proof, 7 No focused proof, 7.3.1 No focused proof (No proof-editing in progress), 7.1.6, 7.2.1 No focused proof to restart, 7.2.2 | No matching clauses for match, 9.2 No matching clauses for match goal, 9.2 No primitive equality found, 8.5.6 No product even after head-reduction, 8.3.1 No such assumption, 8.2.2, 8.4.7 No such binder, 8.1.1 No such goal, 7.3.1 No such hypothesis, 8.3.1, 8.3.3, 8.3.4, 8.3.5, 8.3.6, 8.7.8 No such hypothesis in current goal, 8.3.1, 8.3.1 No such label ident, 2.5.2 Non exhaustive pattern-matching, 17.7 Non strictly positive occurrence of ident in type, 1.3.3 Not a discriminable equality, 8.5.6 Not a primitive equality, 8.5.7 Not a projectable equality but a discriminable one, 8.5.7 Not a proposition or a type, 8.4.1 Not a valid (semi)ring theory, 24.9.2 Not a variable or hypothesis, 8.12.5 Not an evar, 8.12.3 Not an exact proof, 8.2.1 Not an inductive goal with 1 constructor, 8.2.6, 8.2.6 Not an inductive goal with 2 constructors, 8.2.6 Not an inductive product, 8.2.6, 8.5.2 Not convertible, 8.6.9 Not enough constructors, 8.2.6 Not equal, 8.12.1 Not reducible, 8.7.2 Not the right number of induction arguments, 8.5.5 Not the right number of missing arguments, 8.1.1, 8.2.4 Not unifiable, 8.12.2 Nothing to do, it is an equality between convertible terms, 8.5.7 name ident is already used, 8.3.1 no such entry, 6.7.1 not a context variable, 9.2 not a defined object, 6.1.1 not a valid ring equation, 24.4 not declared, 8.9.1, 18.6.1 omega can’t solve this system, 20.1.2 omega: Can’t solve a goal with equality on type, 20.1.2 omega: Can’t solve a goal with non-linear products, 20.1.2 omega: Can’t solve a goal with proposition variables, 20.1.2 omega: Not a quantifier-free goal, 20.1.2 omega: Unrecognized atomic proposition: prop, 20.1.2 omega: Unrecognized predicate or connective: ident, 20.1.2 omega: Unrecognized proposition, 20.1.2 Proof is not complete, 8.4.1, 9.2 quote: not a simple fixpoint, 8.15.2, 10.3 Records declared with the keyword Record or Structure cannot be recursive., 2.1 ring operation should be declared as a morphism, 24.5 Signature components for label ident do not match, 2.5.2 Sortclass cannot be a source class, 18.6.1 Statement without assumptions, 8.2.5 Tactic Failure message (level n), 9.2 Tactic generated a subgoal identical to the original goal, 8.6.1 The numth argument of ident must be ident’ in type, 1.3.3 The conclusion is not a substitutive equation, 8.6.4 The conclusion of type is not valid; it must be built from ident, 1.3.3 The file ident.vo contains library dirpath and not library dirpath’, 6.5.1 The recursive argument must be specified, 2.3 The reference qualid was not found in the current environment, 6.3.7, 6.11.1, 6.11.2 The term form has type … which should be Set, Prop or Type, 1.3.5 The term provided does not end with an equation, 8.6.1 The variable ident is already defined, 8.3.7 This is not the last opened module, 2.5.2 This is not the last opened module type, 2.5.5 This is not the last opened section, 2.4.2 terms do not have convertible types, 8.6.3 Unable to apply, 8.2.5 Unable to find an instance for the variables ident … ident, 8.2.4 Unable to find an instance for the variables ident …ident, 8.5.2 Universe inconsistency, 4.1.1 Variable ident is already declared, 8.4.1