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