-
ident2 not found, 1
- identi not found, 1
- ident already exists, 1, 1, 1, 1, 1
- ident not found, 1
- A record cannot be recursive, 1
- A Setoid Theory is already declared for A, 2
- All terms must have the same type, 1
- Argument of match does not evaluate to a term, 2
- Attempt to save an incomplete proof, 1
- already exists, 2
- Bad magic number, 3
- Bound head variable, 1, 1
- Can't find file ident on loadpath, 1
- Can't find module toto on loadpath, 2
- Cannot find the source class of qualid, 6
- Cannot infer a term for this placeholder, 1, 3
- Cannot load ident: no physical path bound to dirpath, 1
- Cannot move ident1 after ident2:
it depends on ident2, 3
- Cannot move ident1 after ident2:
it occurs in ident2, 2
- Cannot recognize class1 as a source class of qualid, 7
- Cannot refine to conclusions with meta-variables, 2
- Cannot solve the goal, 9.2
- cannot be used as a hint, 2, 2
- Delta must be specified before, 1
- Don't know what to do with this goal, 2
- does not denote an evaluable constant, 1
- does not respect the inheritance uniform condition, 8
- Failed to progress, 9.2
- File not found on loadpath : string, 1
- Found target class class instead of class2, 9
- Funclass cannot be a source class, 3
- generated subgoal term' has metavariables in it, 2
- goal does not satisfy the expected preconditions, 2
- I couldn't solve goal, 2
- I don't know how to handle dependent equality, 1
- Impossible to unify ... with .., 2
- Impossible to unify ... with ..., 1, 9
- In environment ... the term: term2 does not have type
term1, 1
- invalid argument, 1
- is
used in the hypothesis, 3
- is already a coercion, 2
- is already used, 2, 2
- is not a function, 5
- is not a module, 1
- is not a projectable equality, 1
- is not an inductive type, 1
- is used in the
conclusion, 2
- Loading of ML object file forbidden in a native Coq, 2
- Module/section module not found, 2(a)
- must be a transparent constant, 1
- No applicable tactic, 9.2
- No Declared Ring Theory for term., 3
- No discriminable equalities, 2(a)
- No focused
proof, 7
- No focused proof, 1(b)
- No focused proof (No proof-editing in progress), 1, 1
- No focused proof to restart, 1
|
- No matching clauses for match, 1
- No matching clauses for match goal, 9.2
- No product even after head-reduction, 1, 6(a), 7(a)
- No proof-editing in progress, 1
- No such assumption, 1, 1
- No such goal, 1(a)
- No such hypothesis, 6(b), 7(b), 1, 1(a)
- No such hypothesis in current goal, 4, 5
- No such label ident, 1
- No such proof, 1
- Non exhaustive pattern-matching, 2
- Non strictly positive occurrence of ident in type, 1
- Not a discriminable equality, 1
- Not a proposition or a type, 1
- Not a valid (semi)ring theory, 1
- Not a valid setoid theory, 1
- Not an equation, 2
- Not an exact proof, 1
- Not an inductive product, 1, 1
- Not convertible, 1
- Not enough constructors, 2
- Not reducible, 1
- Not the right number of dependent arguments, 6
- Not the right number of missing arguments, 1
- Nothing to rewrite in ident, 1(b)
- name ident is already used, 2
- no such entry, 1
- not a context variable, 9.2
- not a defined object, 1
- not declared, 2, 1
- omega can't solve this system, 1
- omega: Can't solve a goal with equality on type, 8
- omega: Can't solve a goal with non-linear products, 7
- omega: Can't solve a goal with proposition variables, 5
- omega: Not a quantifier-free goal, 2
- omega: Unrecognized atomic proposition: prop, 4
- omega: Unrecognized predicate or connective: ident, 3
- omega: Unrecognized proposition, 6
- Proof is not complete, 9.2
- quote: not a simple fixpoint, 1, 1
- Reached begin of command history, 1
- Signature components for label ident do not match, 2
- Sortclass cannot be a source class, 4
- Tactic Failure "message" (level n), 9.2
- Tactic generated a subgoal identical to the original goal, 2
- The numth argument of ident must be ident' in type, 1
- The conclusion is not a substitutive equation, 1
- The conclusion of type is not valid; it must be
built from ident, 2
- The reference qualid was not found in the current
environment, 1, 1, 1, 1
- The term term is already declared as a morphism, 1
- The term term is not a product, 2
- The term term should not be a dependent product, 3
- The term provided does not end with an equation, 1
- This goal is not an equality, 1
- This is not the last opened module, 3
- This is not the last opened module type, 1
- This is not the last opened section, 1
- the term form has type ... which should be Set,
Prop or Type, 1, 1
- Undo stack would be exhausted, 2
|
