Index of Error Messages
- A goal should be a type *
- A record cannot be recursive *
- All terms must have the same type *
- Attempt to save an incomplete proof *
- Bad explicitation number *
- Bad magic number *
- Bound head variable *, *
- Can not set transparent. *
- Can't find file ident on loadpath *
- Can't find module toto on loadpath *
- Cannot attach a realizer to a logical goal *
- Cannot move ident1 after ident2:
it depends on ident2 *
- Cannot move ident1 after ident2:
it occurs in ident2 *
- Cannot refine to conclusions with meta-variables *, *
- Cannot solve the goal. *
- Clash with previous constant ... *
- Clash with previous constant ident *, *, *, *, *, *
- cannot be used as a hint *, *
- cannot reset to a nonexistent object *
- convert-concl rule passed non-converting term *
- Delta must be specified before *
- Does not correspond to a coercion *
- Don't know what to do with this goal *
- does not exist. *, *
- does not occur *
- does not respect the inheritance uniform condition *
- Failed to progress *
- Found n classical proof(s) but no intuitionistic one *
- FUNCLASS cannot be a source class *
- goal does not satisfy the expected preconditions *, *
- Impossible to unify ... With .. *
- Impossible to unify ... with ... *, *
- In environment ...the term: term2 does not have type
term1 *
- invalid argument *
- is already a class *
- is already a coercion *
- is not a projectable equality *
- is not among the assumptions. *
- is not an inductive type *
- must be a transparent constant *
- No applicable tactic. *
- No Declared Ring Theory for term. *
- No equality here *
- No focused proof *, *
- No focused proof (No proof-editing in progress) *
- No focused proof to restart *
- No product even after head-reduction *, *, *
- No program associated to this subgoal *
- No proof-editing in progress *
- No such assumption *, *
- No such goal *
- No such hypothesis *, *, *
- No such hypothesis in current goal *, *
- No such proof *
- Non informative term *
- Non strictly positive occurrence of ident in type *
- Not a discriminable equality *, *, *
- Not a predefined equality *
- Not a proposition or a type *
- Not a valid (semi)ring theory *
- Not an equation *, *
- Not an exact proof *
- Not an inductive product *, *
- Not enough Constructors *
- Not provable in Direct Predicate Calculus *
- Not reducible *
- Not the right number of dependent arguments *
- Not the right number of missing arguments *
- name ident is already bound *
- not declared *, *, *, *
- 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:prop *
- Omega: Unrecognized predicate or connective:ident *
- Omega: Unrecognized proposition *
- Perhaps a term of the Realizer is not an FW
term *
- Prolog failed *
- Proof objects can only be abstracted *
- Quote: not a simple fixpoint *, *
- repeated goal not permitted in refining mode *
- Section ident does not exist (or is already closed) *
- Section ident is not the innermost section *
- SORTCLASS cannot be a source class *
- Term not reducible *
- The target class does not correspond to ident2 *
- There is an unknown subterm I cannot solve *, *
- This goal is not an equality *
- Type of ident does not end with a sort *
- Type of Constructor not well-formed *
- Type of program and informative extraction of goal do not coincide *
- Undo stack would be exhausted *
- We do not find the source class ident1 *
- 1
- This research was partly supported by ESPRIT Basic Research
Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.
- 1
- This is similar to the
expression ``symbol { sep symbol }'' in
standard BNF, or``symbol ( sep symbol )*'' in
the syntax of regular expressions.
- 1
- These constructions are defined in the
Prelude module in directory theories/INIT at the Coq
root directory; this includes the modules
Logic,
Datatypes,
Specif,
Peano,
and Wf
plus the module Logic_Type
- 1
- This requirement could be relaxed if we instead introduced
an explicit mechanism for instantiating constants. At the external
level, the Coq engine works accordingly to this view that all the
definitions in the environment were built in a sub-context of the
current context.
- 1
- Recall: opaque constants will not be expanded by
d reductions
- 1
-
We omit the lexing step, which simply translates a character stream
into a token stream. If this translation fails, this is a
Lexical error.
- 2
- This syntax is defined in module LogicSyntax
- 3
- They are in Datatypes.v
- 4
- They are defined in module Specif.v
- 5
- This syntax can be found in the module
SpecifSyntax.v
- 6
- This is in module Peano.v
- 7
- This is defined in module Wf.v
- 8
- This is in module
Logic_Type.v
- 9
- This syntax is defined in module Logic_TypeSyntax
- 10
- http://coq.inria.fr
- 1
- This research was partly supported by ESPRIT Basic Research
Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.
- 1
- In languages of the ML family the first definition would
be translated into a term where the variable x is shared in
the expression. When patterns are of non-dependent types, Coq
compiles as in ML languages using sharing. When patterns are of
dependent types the compilation reconstructs the term as in the
second definition of last so to ensure the result of
expansion is well typed.
- 1
- It
corresponds to Fw plus inductive definitions
- 1
- Should
you obtain a not ML-typable program out of a self developed example,
we would be interested in seeing it; so please mail us the example at
coq@pauillac.inria.fr
- 2
- except
if no equation is given, to match the term in an empty type, e.g. the
type False
- 2
- Actually, (Rel n) means that (n-1) binders
have to be traversed, since indexes are represented by strictly
positive integers.
- 2
- This information is not strictly needed but
was useful for type checking in a first experiment.
This document was translated from LATEX by HEVEA.