CODEWITHSUNDEEP
coq
Jan Tušil
Jan Tušil

Reputation: 978

Unable to satisfy the following constraints: In environment

In proof editing mode, in use of the apply tactic, Coq gives me the following error message:

Error:
Unable to satisfy the following constraints:
In environment:
signature : Signature
X : gset evar

?MLVariables : "MLVariables"

?H : "FMap (gmap evar)"

?H0 : "forall A : Type, Lookup evar A (gmap evar A)"

?H1 : "forall A : Type, Empty (gmap evar A)"

?H2 : "forall A : Type, PartialAlter evar A (gmap evar A)"

?H3 : "OMap (gmap evar)"

?H4 : "Merge (gmap evar)"

?H5 : "forall A : Type, FinMapToList evar A (gmap evar A)"

?EqDecision0 : "RelDecision eq"

?H6 : "FinMap evar (gmap evar)"

How to read this message? What confuses me is that there is nothing between the lines

Unable to satisfy the following constraints:
In environment:

where I would expect the list of unsatisfied constraints. Is the list of unsatisfied constraints given after the In environment: block? I.e., every line starting with a question mark variable shows one unsatisfied constraint? Another option would be that coq is trying to tell me there is an empty set of unsatisfied constraint, printed before the environment.

Upvotes: 1

Views: 283

Answers (1)

dlesbre
dlesbre

Reputation: 517

This message is a bit misleading, the constraints it can't satisfy are those starting with a question mark ?. In short you can read the message as follows:

Error: In environment: // This is just debug information
signature : Signature
X : gset evar

Unable to satisfy the following constraints: 
// These are the missing terms Coq can't guess
?MLVariables : "MLVariables"
?H : "FMap (gmap evar)"
?H0 : "forall A : Type, Lookup evar A (gmap evar A)"
?H1 : "forall A : Type, Empty (gmap evar A)"
?H2 : "forall A : Type, PartialAlter evar A (gmap evar A)"
?H3 : "OMap (gmap evar)"
?H4 : "Merge (gmap evar)"
?H5 : "forall A : Type, FinMapToList evar A (gmap evar A)"
?EqDecision0 : "RelDecision eq"
?H6 : "FinMap evar (gmap evar)"

Upvotes: 1

Related Questions