coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dealing with setoid rewriting problems

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] dealing with setoid rewriting problems
Date: Mon, 30 Nov 2015 16:02:40 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-pa0-f50.google.com
Ironport-phdr: 9a23:IeGzKxdFPgdBui6r+++EaOU8lGMj4u6mDksu8pMizoh2WeGdxc65ZR7h7PlgxGXEQZ/co6odzbGG7uawCCdZsN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvc2CKFwZzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB1sfnhtNSzrM6BDkV9+lrDnzsutj0QGRONCwQLwpD2fxp5x3QQPl3X9UfwUy93va35R9

> On Nov 30, 2015, at 15:55 , Clément Pit--Claudel
> <clement.pit AT gmail.com>
> wrote:
>
> Could this be https://coq-bench.github.io/ (courtesy of Guillaume Claret)?

Yes thats the page. Thanks!

Unfortunately both CoLoR and math-classes are shown as “not compatible” with
recent 8.5 betas so I am stuck with 8.4 for now and need to find a way to
solve this problem under 8.4.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva

[Coq-Club] dealing with setoid rewriting problems, Vadim Zaliva, 12/01/2015
- Re: [Coq-Club] dealing with setoid rewriting problems, Clément Pit--Claudel, 12/01/2015
  - Re: [Coq-Club] dealing with setoid rewriting problems, Vadim Zaliva, 12/01/2015
    - Re: [Coq-Club] dealing with setoid rewriting problems, Abhishek Anand, 12/01/2015
      - Re: [Coq-Club] dealing with setoid rewriting problems, Vadim Zaliva, 12/01/2015
        
        Re: [Coq-Club] dealing with setoid rewriting problems, Vadim Zaliva, 12/01/2015
        
        Re: [Coq-Club] dealing with setoid rewriting problems, James Lottes, 12/01/2015
        
        Re: [Coq-Club] dealing with setoid rewriting problems, Pierre Courtieu, 12/01/2015