Specification language
match
in
type_scope
function_scope
Arguments
Proofs
Proof using
Scheme
Derive
Inversion
dependent destruction
dependent induction
lra
lia
nra
nia
psatz
zify
nsatz
Type
L
Using Coq
Functional
coqrc
-vos
Appendix
"All" is a predefined collection containing all variables. It can't be redefined
'via' and 'abstract' cannot be used together
... is not definitionally an identity function
A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.17)
Activation of abbreviations does not expect mentioning a grammar entry
Activation of abbreviations does not expect mentioning a scope
Argument at position ‘natural’ is mentioned more than once
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 given by name or position not supported in explicit mode
Arguments of ring_simplify do not have all the same type
Arguments of section variables such as ‘name’ may not be renamed
Attempt to save an incomplete proof
Automatically declaring ‘ident’ as template polymorphic
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
Cannot build functional inversion principle
Cannot change ‘ident’, it is used in conclusion
Cannot change ‘ident’, it is used in hypothesis ‘ident’
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 a relation to rewrite
Cannot find any non-recursive equality over ‘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 find the target class
Cannot import local constant, it will be ignored
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 a statement based on ‘reference’
Cannot recognize ‘coercion_class’ as a source class of ‘qualid’
Cannot turn [inductive|constructor] into an evaluable reference
Cannot use mutual definition with well-founded recursion or measure
Can’t find file ‘ident’ on loadpath
Casts are not supported in this pattern
Compiled library ‘ident’.vo makes inconsistent assumptions over library ‘qualid’
Condition not satisfied
Debug mode not available in the IDE
Declaring arbitrary terms as hints is fragile; it is recommended to declare a toplevel constant instead
Duplicate clear of H. Use { }H instead of { H }H
Dynlink error: execution of module initializers in the
Either there is a type incompatibility or the problem involves dependencies
Expression does not evaluate to a tactic
Failed to progress
File ... found twice in ...
File not found on loadpath: ‘string’
Files processed by Load cannot leave open proofs
Flag 'rename' expected to rename ‘name’ into ‘name’
Found a constructor of inductive type term while a constructor of term is expected
Found an "at" clause without "with" clause
Found no matching notation to enable or disable
Found no subterm matching ‘term’ in the current goal
Found no subterm matching ‘term’ in ‘ident’
Found target class ‘coercion_class’ instead of ‘coercion_class’
Funclass cannot be a source class
Goal is solvable by congruence but some arguments are missing. Try congruence with ‘term’…‘term’, replacing metavariables by arbitrary terms
Hypothesis ‘ident’ must contain at least one Function
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
Incorrect number of tactics (expected N tactics, was given M)
Invalid backtrack
lapply needs a non-dependent product
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
Ltac2 alias ‘qualid’ is deprecated since ‘string’. ‘string’
Ltac2 definition ‘qualid’ is deprecated since ‘string’. ‘string’
Ltac2 notation ‘ltac2_scope’…‘ltac2_scope’ is deprecated since ‘string’. ‘string’
Making shadowed name of implicit argument accessible by position
Missing mapping for constructor ‘qualid’
Module/section ‘qualid’ not found
More than one interpretation bound to this notation, confirm with the "all" modifier
Multiple 'via' options
Multiple 'warning after' or 'abstract after' options
Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on
New coercion path ... is ambiguous with existing ...
New Collection definition of ‘ident’ shadows the previous one
No applicable tactic
No argument name ‘ident’
No evars
No field named ‘ident’ in ‘qualid’
No focused proof
No focused proof (No proof-editing in progress)
No focused proof to restart
No head constant to reduce
No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop. You can try to use option Set Keep Proof Equalities
No matching clauses for match
No matching clauses for match goal
No notation provided
No primitive equality found
No product even after head-reduction
No progress made
No quantified hypothesis named ‘ident’ in current goal even after head-reduction
No such assumption
No such binder
No such bound variable ‘ident’ (no bound variables at all in the expression)
No such bound variable ‘ident’ (possible names are: ‘ident’ ...)
No such goal
No such goal (‘ident’)
No such goal (‘natural’)
No such goal. (fail)
No such goal. (Goal selector)
No such goal. Focus next goal with bullet ‘bullet’
No such goal. Try unfocusing with }
No such hypothesis: ‘ident’
No ‘natural’-th non dependent hypothesis in current goal even after head-reduction
Non exhaustive pattern matching
Non extensible universe declaration not supported with monomorphic Program Definition
Non strictly positive occurrence of ‘ident’ in ‘type’
not a cofix definition
not a constant
not a constructor
Not a context variable
Not a discriminable equality
not a fix definition
Not a negated primitive equality
not a primitive projection
Not a valid ring equation
Not a variable or hypothesis
not an (co)inductive datatype
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 enough non implicit arguments to accept the argument bound to ‘ident’
Not enough non implicit arguments to accept the argument bound to ‘natural’
Not equal
Not equal (due to universes)
Not ground
Not the right number of induction arguments
Not the right number of missing arguments (expected ‘natural’)
Notation levels must range between 0 and 6
Notation ‘string’ is deprecated since ‘string’. ‘string’
Nothing to inject
Nothing to rewrite
overflow in int63 literal ‘bigint’
package-name.foo and not foo_plugin
plugin name anymore. Plugins should be loaded using their
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)
public name according to findlib, for example
Records declared with the keyword Record or Structure cannot be recursive
Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one
Required library ‘qualid’ matches several files in path (found file.vo, file.vo, ...)
Ring operation should be declared as a morphism
Section variable ‘ident’ occurs implicitly in global declaration ‘qualid’ present in hypothesis ‘ident’
Section variable ‘ident’ occurs implicitly in global declaration ‘qualid’ present in the conclusion
shared library failed: Coq Error: ‘string’ is not a valid
Signature components for field ‘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)
Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command])
Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command])
Tactic failure
Tactic failure (level ‘natural’)
Tactic failure: <tactic closure> succeeds
Tactic failure: Setoid library not loaded
Tactic generated a subgoal identical to the original 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 "at" syntax isn't available yet for the autorewrite tactic
The & modifier may only occur once
The 'abstract after' directive has no effect when the parsing function (‘qualid’) targets an option type
The 'clear implicits' flag must be omitted if implicit annotations are given
The 'default implicits' flag is incompatible with implicit annotations
The / modifier may only occur once
The command has not failed!
The conclusion of ‘type’ is not valid; it must be built from ‘ident’
The constant ‘number’ is not a binary64 floating-point value. A closest value ‘number’ will be used and unambiguously printed ‘number’. [inexact-float,parsing]
The constructor ‘ident’ expects ‘natural’ arguments
The cumulative attribute can only be used in a polymorphic context
The elimination predicate term should be of arity ‘natural’ (for non dependent case) or ‘natural’ (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 relation ‘ident’ is not a declared reflexive relation. Maybe you need to require the Coq.Classes.RelationClasses library
The relation ‘ident’ is not a declared symmetric relation. Maybe you need to require the Coq.Classes.RelationClasses library
The relation ‘ident’ is not a declared transitive relation. Maybe you need to require the Coq.Classes.RelationClasses library
The term "‘type’" has type "‘type’" which should be Set, Prop or Type
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 has no constructors
The type ‘ident’ must be registered before this construction can be typechecked
The variable ident is bound several times in pattern term
The variable ‘ident’ is already declared
The ‘natural’ th argument of ‘ident’ must be ‘ident’ in ‘type’
There is already an Ltac named ‘qualid’
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 Ltac named ‘qualid’
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 hint is not local but depends on a section variable. It will disappear when the section is closed
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’
To rename arguments the 'rename' flag must be specified
Trying to mask the absolute name ‘qualid’!
Type of ‘ident’ is not an equality of recognized Σ types: expected one of sig sig2 sigT sigT2 sigT2 ex or ex2 but got ‘term’
Type of ‘qualid’ seems incompatible with the type of ‘qualid’. Expected type is: ‘type’ instead of ‘type’. This might yield ill typed terms when using the notation
Unable to apply lemma of type "..." on hypothesis of type "..."
Unable to find an instance for the variables ‘ident’ … ‘ident’
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 ‘one_term’ with ‘one_term’
Unbound [value|constructor] X
Unbound context identifier ‘ident’
Undeclared universe ‘ident’
Unexpected non-option term ‘term’ while parsing a number notation
Unexpected non-option term ‘term’ while parsing a string notation
Unexpected only parsing for an only printing notation
Unexpected only printing for an only parsing notation
Unexpected term ‘term’ while parsing a number notation
Unexpected term ‘term’ while parsing a string notation
Universe inconsistency
Universe instance length is ‘natural’ but should be ‘natural’
Unknown custom entry
Unknown custom entry: ‘ident’
Unknown inductive type
Unused variable ‘ident’ might be a misspelled constructor. Use _ or _‘ident’ to silence this warning.
Use of ‘string’ Notation is deprecated as it is inconsistent with pattern syntax
Variable All is shadowed by Collection named All containing all variables
Wrong argument name
Wrong argument position
Wrong bullet ‘bullet’: Bullet ‘bullet’ is mandatory here
Wrong bullet ‘bullet’: Current bullet ‘bullet’ is not finished
‘coercion_class’ must be a transparent constant
‘ident’ already exists
‘ident’ already exists. (Axiom)
‘ident’ already exists. (Definition)
‘ident’ already exists. (Theorem)
‘ident’ cannot be defined
‘ident’ cannot be defined because it is informative and ‘ident’ is not
‘ident’ cannot be defined because the projection ‘ident’ was not defined
‘ident’ is already declared as a typeclass
‘ident’ is already used
‘ident’ is both name of a Collection and Variable, Collection ‘ident’ takes precedence over Variable
‘ident’ is declared as a local axiom
‘ident’ is declared opaque but this is not fully respected inside the section and not at all outside the section
‘ident’ is not a local definition
‘ident’ is not an equality of Σ types
‘ident’ is opaque
‘ident’ is used in the conclusion
‘ident’ is used in the hypothesis ‘ident’
‘ident’ was already a defined Variable, the name ‘ident’ will refer to Collection when executing "Proof using" command
‘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 Number.int to ‘type’ or (option ‘type’). Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or PrimFloat.float or Number.number could be used (you may need to require BinNums or Number or PrimInt63 or PrimFloat 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 Number.int or (option Number.int). Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first)
‘qualid’ was already mapped to ‘qualid’ and cannot be remapped to ‘qualid’
‘string’ cannot be interpreted as a known notation in ‘ident’ entry. Make sure that symbols are surrounded by spaces and that holes are explicitly denoted by "_"
‘string’ cannot be interpreted as a known notation. Make sure that symbols are surrounded by spaces and that holes are explicitly denoted by "_"
‘type’ is not an inductive type
‘type’ was already mapped to ‘type’, mapping it also to ‘type’ might yield ill typed terms when using the notation