search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Reify.v invalidates valid syntax #100

Open jesper-bengtson opened 7 years ago

jesper-bengtson commented 7 years ago

After importing MirrorCore.Reify.Reify the following command stops working:

Implicit Arguments id [[A] [B] ...]

Implicit Arguments is deprecated and Arguments should be used in stead, but it is still valid Coq syntax that does not work.

gmalecha commented 7 years ago

I agree this is a problem. In the meantime, you should change Implicit Arguments into Arguments or put a space between the two [s.