-
ident2 not found, 1
- identi not found, 1
- ident already exists, 1, 1, 1, 1, 1, 1
- ident not found, 1
- A record cannot be recursive, 1
- Argument of match does not evaluate to a term, 2
- Attempt to save an incomplete proof, 1
- already exists, 2
- arguments of ring_simplify do not have all the same type, 2
- Bad magic number, 3
- Bound head variable, 1, 1
- bad lemma for decidability of equality, 2
- bad ring structure, 1
- Can't find file ident on loadpath, 1
- Can't find module toto on loadpath, 2
- Cannot build functional inversion principle, 6
- Cannot define graph for ident…, 4
- Cannot define principle(s) for ident…, 5
- Cannot find induction information on qualid, 1
- Cannot find inversion information for hypothesis ident, 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 use mutual definition with well-founded
recursion or measure, 3
- cannot be used as a hint, 2, 2
- cannot find a declared ring structure for equality
term, 4
- cannot find a declared ring structure over term, 3
- Delta must be specified before, 1
- does not denote an evaluable constant, 1
- does not respect the inheritance uniform condition, 8
- Error: The term “term” has type type while it is expected to have type “type”, 1
- 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
- Goal is solvable by congruence but some arguments are missing. Try congruence with …, replacing metavariables by arbitrary terms., 3
- generated subgoal term' has metavariables in it, 2
- goal does not satisfy the expected preconditions, 2
- Hypothesis identmust contain at least one Function, 1
- 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, 10
- 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 argument name ident, 2
- 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
- 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 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, 7
- Not the right number of induction arguments, 2
- Not the right number of missing arguments, 1
- name ident is already used, 2
- no such entry, 1
- not a context variable, 9.2
- not a defined object, 1
- not a valid ring equation, 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
- ring operation should be declared as a morphism, 3
- Signature components for label ident do not match, 2
- Sortclass cannot be a source class, 4
- Statement without assumptions, 1
- 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 recursive argument must be specified, 1
- The reference qualid was not found in the current
environment, 1, 1, 1, 1
- The term provided does not end with an equation, 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
- terms do not have convertible types, 1
- the term form has type … which should be Set,
Prop or Type, 1, 1
- Unable to apply, 2
- Undo stack would be exhausted, 2
- Universe
inconsistency, 4.1.1
|
