-
ident already exists, 1.3.1, 1.3.1, 1.3.2, 1.3.2, 1.3.5, 24.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, 25.4
- Bad magic number, 6.5.1
- bad lemma for decidability of equality, 25.5
- bad ring structure, 25.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.14.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
- Condition not satisfied, 9.2
- cannot be used as a hint, 8.9.1, 8.9.1
- cannot find a declared ring structure for equality
term, 25.4
- cannot find a declared ring structure over term, 25.4
- does not denote an evaluable constant, 8.7.5
- does not respect the uniform inheritance condition, 18.6.1
- Failed to progress, 9.2
- File not found on loadpath : , 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.14.1
- I don’t know how to handle dependent equality, 8.10.5
- In environment … the term: term2 does not have type
term1, 24.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.7
- 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.11.4
- No focused
proof, 7
- No focused proof, 7.3.1
- No focused proof (No proof-editing in progress), 7.1.6
- 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 progress made, 27.4.2
- No such assumption, 8.2.2, 8.4.7
- No such binder, 8.1.3
- No such goal, 7.3.1, 9.2
- No such goal. Focus next goal with bullet
bullet., 7.2.7
- No such goal. Try unfocusing with }., 7.2.7
| - 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 variable or hypothesis, 8.11.5
- Not an evar, 8.11.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.5
- Not enough constructors, 8.2.6
- Not equal, 8.11.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.3, 8.2.4
- Not unifiable, 8.11.2
- Nothing to do, it is an equality between convertible terms, 8.5.7
- Nothing to rewrite, 27.4.2
- 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, 25.4
- not declared, 18.6.1
- omega can’t solve this system, 21.1.2
- omega: Can’t solve a goal with equality on type, 21.1.2
- omega: Can’t solve a goal with non-linear products, 21.1.2
- omega: Can’t solve a goal with proposition variables, 21.1.2
- omega: Not a quantifier-free goal, 21.1.2
- omega: Unrecognized atomic proposition: prop, 21.1.2
- omega: Unrecognized predicate or connective: ident, 21.1.2
- omega: Unrecognized proposition, 21.1.2
- Proof is not complete, 8.4.1, 9.2
- quote: not a simple fixpoint, 8.14.2, 10.3
- Records declared with the keyword Record or Structure cannot be recursive., 2.1
- Require is not allowed inside a module or a module type, 6.5.1
- ring operation should be declared as a morphism, 25.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.12.2
- 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.6, 6.10.1, 6.10.2
- The term form has type … which should be Set,
Prop or Type, 1.3.5
- The term term has type type while it is expected to have type type, 1.3.2
- 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
- This proof is focused, but cannot be unfocused
this way, 7.2.6
- This tactic has more than one success, 9.2
- terms do not have convertible types, 8.6.2
- 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
- Unable to satisfy the rewriting constraints, 27.4.2
- Unable to unify … with …, 8.2.4, 8.12.2
- Undeclared universe ident, 29.6.2
- Universe
inconsistency, 4.1.1
- Universe inconsistency, 29.6.2
- Variable ident is already declared, 8.4.1
- Wrong bullet bullet1 : Bullet bullet2
is mandatory here., 7.2.7
- Wrong bullet bullet1 : Current bullet
bullet2 is not finished., 7.2.7
|