The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

I'm doing a proof and I get this error.

Coq < Load reference.
Error while reading /Users/mulhern/mulhern/cs/pierce_test/reference.v :
File "/Users/mulhern/mulhern/cs/pierce_test/reference.v", line 229,
characters 39-54
Error:
In environment
eval : term * store -> term * store -> Prop
t : term
s : store
s' : store
H : isval t
The term "exist isval t H" has type "sig isval"
while it is expected to have type "Store.V"

But Store.V = sig isval as I can tell by this succession of Print statements.

Coq < Print Store.V
Coq < .
Store.V = ValExp.A
    : Set


Coq < Print ValExp.A.
ValExp.A = {t : term | isval t}
    : Set

How can I make the Coq compiler use that information which it so
clearly possesses?

Store looks like this:

Coq < Print Store.
Module Store
 : Sig
     Definition V
     ....
     Definition allocate
   End
 := (Map_Wf_Ext Val)

ValExp looks like this:

Coq < Print ValExp.
Module ValExp
 : Sig
     Definition A
     Definition equal
     Parameter equal_refl
     Parameter equal_sym
     Parameter equal_trans
     Parameter equal_dec
   End
 := Struct
      Definition A
      Definition equal
      Theorem equal_refl
      Theorem equal_sym
      Theorem equal_trans
      Theorem equal_dec
    End

Map_Wf_Ext looks like this:

Coq < Print Map_Wf_Ext.
Module Map_Wf_Ext
 : Funsig (Val : VALUE)
     Sig
       Definition V
       ...
       Definition allocate
     End
 := Functor [Val:VALUE]
      Struct
        Definition V
        ....
        Definition allocate
      End

And VALUE looks like this.

Coq < Print VALUE.
Module Type VALUE = Sig
                     Parameter A
                     Parameter equal
                     Parameter equal_dec
                     Parameter equal_refl
                     Parameter equal_sym
                     Parameter equal_trans
                   End

-mulhern