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 ident₁ after ident₂: it depends on ident₂  *
• Cannot move ident₁ after ident₂: it occurs in ident₂  *
• 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: term₂ does not have type term₁  *
• 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 ident₂  *
• 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 ident₁  *

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 F_w 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 L^AT_EX by H^EV^EA.