Errors and Warnings Index

. | @ | a | b | c | d | e | f | g | h | i | l | m | n | o | p | r | s | t | u | v | w | y |
 
.
... is not definitionally an identity function
 
@
@ident already exists. (Axiom)
@ident already exists. (Definition)
@ident already exists. (Program Definition)
@ident already exists. (Theorem)
 
a
Argument of match does not evaluate to a term
Argument ‘name’ is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]
Arguments of ring_simplify do not have all the same type
Attempt to save an incomplete proof
Automatically declaring ‘ident’ as template polymorphic
 
b
Bad lemma for decidability of equality
Bad magic number
Bad occurrence number of ‘qualid’
Bad relevance
Bad ring structure
Brackets do not support multi-goal selectors
 
c
Cannot build functional inversion principle
Cannot coerce ‘qualid’ to an evaluable reference
Cannot define graph for ‘ident’
Cannot define principle(s) for ‘ident’
Cannot find a declared ring structure for equality ‘term’
Cannot find a declared ring structure over ‘term’
Cannot find any non-recursive equality over :n:`‘ident’`
Cannot find induction information on ‘qualid’
Cannot find inversion information for hypothesis ‘ident’
Cannot find library foo in loadpath
Cannot find the source class of ‘qualid’
Cannot handle mutually (co)inductive records
Cannot infer a term for this placeholder. (Casual use of implicit arguments)
Cannot infer a term for this placeholder. (refine)
Cannot interpret in ‘scope_name’ because ‘qualid’ could not be found in the current environment
Cannot interpret this number as a value of type ‘type’
Cannot interpret this string as a value of type ‘type’
Cannot load ‘qualid’: no physical path bound to ‘dirpath’
Cannot move ‘ident’ after ‘ident’: it depends on ‘ident’
Cannot move ‘ident’ after ‘ident’: it occurs in the type of ‘ident’
Cannot recognize a boolean equality
Cannot recognize ‘class’ as a source class of ‘qualid’
Cannot use mutual definition with well-founded recursion or measure
Can’t find file ‘ident’ on loadpath
Compiled library ‘ident’.vo makes inconsistent assumptions over library ‘qualid’
Condition not satisfied
 
d
Debug mode not available in the IDE
 
e
Either there is a type incompatibility or the problem involves dependencies
Expression does not evaluate to a tactic
 
f
Failed to progress
File not found on loadpath: ‘string’
Files processed by Load cannot leave open proofs
Found target class ... instead of ...
Funclass cannot be a source class
 
g
goal does not satisfy the expected preconditions
Goal is solvable by congruence but some arguments are missing. Try congruence with ‘term’…‘term’, replacing metavariables by arbitrary terms
 
h
Hypothesis ‘ident’ must contain at least one Function
 
i
I don’t know how to handle dependent equality
Ignored instance declaration for “‘ident’”: “‘term’” is not a class
Ignoring implicit binder declaration in unexpected position
Ill-formed recursive definition
Ill-formed template inductive declaration: not polymorphic on any universe
In environment … the term: ‘term’ does not have type ‘type’. Actually, it has type ...
Incorrect number of tactics (expected N tactics, was given M)
Invalid argument
Invalid backtrack
 
l
Last block to end has name ‘ident’
Load is not supported inside proofs
Ltac Profiler encountered an invalid stack (no self node). This can happen if you reset the profile during tactic execution
 
m
Making shadowed name of implicit argument accessible by position
Module/section ‘qualid’ not found
 
n
Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on
New coercion path ... is ambiguous with existing ...
No applicable tactic
No argument name ‘ident’
No discriminable equalities
No evars
No focused proof
No focused proof (No proof-editing in progress)
No focused proof to restart
No head constant to reduce
No matching clauses for match
No matching clauses for match goal
No primitive equality found
No product even after head-reduction
No progress made
No such assumption
No such binder
No such goal
No such goal (‘ident’)
No such goal (‘num’)
No such goal. (fail)
No such goal. (Goal selector)
No such goal. Focus next goal with bullet ‘bullet’
No such hypothesis
No such hypothesis in current goal
No such hypothesis: ‘ident’
No such label ‘ident’
Non exhaustive pattern matching
Non strictly positive occurrence of ‘ident’ in ‘type’
Not a context variable
Not a discriminable equality
Not a primitive equality
Not a proposition or a type
Not a valid ring equation
Not a variable or hypothesis
Not an evar
Not an exact proof
Not an inductive goal with 1 constructor
Not an inductive goal with 2 constructors
Not an inductive product
Not convertible
Not enough constructors
Not equal
Not equal (due to universes)
Not reducible
Not the right number of induction arguments
Not the right number of missing arguments
Notation ‘string’ is deprecated since ‘string’. ‘string’
Nothing to do, it is an equality between convertible terms
Nothing to inject
Nothing to rewrite
 
o
omega can't solve this system
omega: Can't solve a goal with equality on type ...
omega: Can't solve a goal with non-linear products
omega: Can't solve a goal with proposition variables
omega: Not a quantifier-free goal
omega: Unrecognized atomic proposition: ...
omega: Unrecognized predicate or connective: ‘ident’
omega: Unrecognized proposition
 
p
Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead
Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead
Proof is not complete. (abstract)
Proof is not complete. (assert)
 
r
Records declared with the keyword Record or Structure cannot be recursive
Refine passed ill-formed term
Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one
Ring operation should be declared as a morphism
 
s
Section variable :n:`‘ident’` occurs implicitly in global declaration :n:`‘qualid’` present in hypothesis :n:`‘ident’`
Section variable :n:`‘ident’` occurs implicitly in global declaration :n:`‘qualid’` present in the conclusion
Signature components for label ‘ident’ do not match
SProp is disallowed because the "Allow StrictProp" flag is off
SSReflect: cannot obtain new equations out of ...
Stack overflow or segmentation fault happens when working with large numbers in ‘type’ (threshold may vary depending on your system limits and on the command executed)
Statement without assumptions
Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command])
Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command])
 
t
Tactic failure
Tactic failure (level ‘num’)
Tactic failure: <tactic closure> fails
Tactic failure: <tactic closure> succeeds
Tactic generated a subgoal identical to the original goal. This happens if ‘term’ does not occur in the goal
Tactic Notation ‘qualid’ is deprecated since ‘string’. ‘string’
Tactic ‘qualid’ is deprecated since ‘string’. ‘string’
template and polymorphism not compatible
Terms do not have convertible types
The 'abstract after' directive has no effect when the parsing function (‘qualid’) targets an option type
The / modifier may only occur once
The command has not failed!
The conclusion is not a substitutive equation
The conclusion of ‘type’ is not valid; it must be built from ‘ident’
The constant ‘numeral’ is not a binary64 floating-point value. A closest value ‘numeral’ will be used and unambiguously printed ‘numeral’. [inexact-float,parsing]
The constructor ‘ident’ expects ‘num’ arguments
The cumulative and noncumulative attributes can only be used in a polymorphic context
The elimination predicate term should be of arity ‘num’ (for non dependent case) or ‘num’ (for dependent case)
The field ‘ident’ is missing in ‘qualid’
The file ‘ident’.vo contains library ‘qualid’ and not library ‘qualid’
The recursive argument must be specified
The reference is not unfoldable
The reference X was not found in the current environment
The reference ‘qualid’ was not found in the current environment
The term ‘term’ has type ‘type’ which should be Set, Prop or Type
The term ‘term’ has type ‘type’ while it is expected to have type ‘type’'
The type ‘ident’ must be registered before this construction can be typechecked
The variable ‘ident’ is already defined
The ‘num’ th argument of ‘ident’ must be ‘ident’ in ‘type’
The ‘term’ provided does not end with an equation
There is no flag or option with this name: "‘setting_name’"
There is no flag, option or table with this name: "‘setting_name’"
There is no qualid-valued table with this name: "‘setting_name’"
There is no string-valued table with this name: "‘setting_name’"
There is nothing to end
This command does not support this attribute
This command is just asserting the names of arguments of ‘qualid’. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes'
This object does not support universe names
This proof is focused, but cannot be unfocused this way
This tactic has more than one success
To avoid stack overflow, large numbers in ‘type’ are interpreted as applications of ‘qualid’
Too few occurrences
Trying to mask the absolute name ‘qualid’!
 
u
Unable to apply
Unable to find an instance for the variables ‘ident’…‘ident’
Unable to infer a match predicate
Unable to satisfy the rewriting constraints
Unable to unify ... with ...
Unable to unify ‘term’ with ‘term’
Unbound [value|constructor] X
Unbound context identifier ‘ident’
Undeclared universe ‘ident’
Unexpected non-option term ‘term’ while parsing a numeral notation
Unexpected non-option term ‘term’ while parsing a string notation
Unexpected term ‘term’ while parsing a numeral notation
Unexpected term ‘term’ while parsing a string notation
Universe inconsistency
Universe instance should have length ‘num’
Unknown inductive type
Use of ‘string’ Notation is deprecated as it is inconsistent with pattern syntax
 
v
Variable ‘ident’ is already declared
 
w
When ‘term’ contains more than one non dependent product the tactic lapply only takes into account the first product
Wrong bullet ‘bullet’: Bullet ‘bullet’ is mandatory here
Wrong bullet ‘bullet’: Current bullet ‘bullet’ is not finished
 
y
You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof
 
‘class’ must be a transparent constant
‘ident’ cannot be defined
‘ident’ is already declared as a typeclass
‘ident’ is already used
‘ident’ is declared as a local axiom
‘ident’ is not a local definition
‘ident’ is used in conclusion
‘ident’ is used in hypothesis ‘ident’
‘ident’ is used in the conclusion
‘ident’ is used in the hypothesis ‘ident’
‘ident’: no such entry
‘qualid’ cannot be used as a hint
‘qualid’ does not occur
‘qualid’ does not respect the uniform inheritance condition
‘qualid’ is already a coercion
‘qualid’ is bound to a notation that does not denote a reference
‘qualid’ is not a function
‘qualid’ is not a module
‘qualid’ is not an inductive type
‘qualid’ not a defined object
‘qualid’ not declared
‘qualid’ should go from Byte.byte or (list Byte.byte) to ‘type’ or (option ‘type’)
‘qualid’ should go from Numeral.int to ‘type’ or (option ‘type’). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first)
‘qualid’ should go from ‘type’ to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte))
‘qualid’ should go from ‘type’ to Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first)
‘type’ is not an inductive type