coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)
Date: Wed, 9 Nov 2016 16:47:47 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f196.google.com
Ironport-phdr: 9a23:cGlkPRCz/aZVDO7Ui7svUyQJP3N1i/DPJgcQr6AfoPdwSPvzr8bcNUDSrc9gkEXOFd2CrakV0KyO6+u5ADJIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZb1/IA+qoQnNucUanJZuJ6cswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9VvQyvpxJ/zYDXbo+aOvVxcaHBct0VXmdBQsVcWjZdDo+gYYYCD+wMNvtYoYnnoFsOqAOzCw2rBOPp0DBImn/20rc80+88Fw/Jwg0gH8wQv3TSsNX+KaAfUeKyzKnOzDXDbO1Z2TPj54fWaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik3IoqwVrrTi128cskZPFhocLxV3C6C53w541KMWmREJnZdOoCphduiGAO4doXM8uX3tktDs+x7AHoZK2fjUGxI45yxPRZPGLaZWE7xz/WOqLPzt1inBodbSijBio60eg0PfzVsys3VZKsCVFlt7Mu2gI1xPJ68iHTuJx/l6i2TqTzgzT5PxILEQ1mKbBJJ4hxbkwlpUXsUvdBCP5hEL2jKqOekUl/Oin9fjnb634qpOAM4J4kALzP6Q0lsChH+g0LhICU3Wf9Om9zLHj+Ff2QLROjv04iKnZt5XaKNwZpq6+BQ9V04Uj5Ai7Dzi4ztsVhnYHLFdfdxKGi4jlIU3BIPf9DfunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4ftoi4ffyjXY/0XsQfLek24dfPHK/GPVlLkGUbFLjh94AFSEBuQ9oH7+is0GLTTMGPyX6ZKk7/DxuUI8=

On 11/09/2016 04:30 PM, Clément Pit--Claudel wrote:

...
See my comment on
http://coq-blog.clarus.me/why-and-how-to-write-code-compatible-with-many-coq-versions.html
(maybe?)

GNU m4 is another alternative - it is free of many of the limitations of CPP, and already exists on almost all linuxes. But, one still needs to solve the preprocess-in-between-IDE-and-coqtop issue.

-- Jonathan

[Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/09/2016
- Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
  - RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/09/2016
    - Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
      - Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Clément Pit--Claudel, 11/09/2016
        
        Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
        
        Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Paul A. Steckler, 11/09/2016
      - RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/10/2016