coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using Ssreflect in Coq

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Using Ssreflect in Coq
Date: Wed, 5 Sep 2018 13:51:37 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:mcAe9RQrkB+Nozz6V4YR7qpwD9psv+yvbD5Q0YIujvd0So/mwa69ZBSN2/xhgRfzUJnB7Loc0qyK6/+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/m/XhMJukaxVoxyhqBNjzIHJb4+aNvRxc7jBfd4ZX2dNQtpdWjZcDo66coABD/ABPeFdr4TlqFUOqwG+BQiwC+Po1zRGmGX53bYh0+QgDArL2xIvH9QUsHTVsNr1M70eUfyvw6nT1jXDbuhb2Tb76IjScxAuu+uAXbxqccfIz0QkCgDLjk2IpIHhMD6ZzPoBvmaB4+dhUe+jkXMrpx9zrzS328shhIrEipgRx13F7yl0z4U4KcelREJlfNKpFoZbuTuAOItsWMwiRnlluCYkxb0Cvp62ZCYKx4o7xx7DdvyHdZSI7Qj5WOaWOzd4i2ppeLO5hxms7Uit0unxW8au3FpUoCdJiNjBu3QX2xDO9MSKSONx/kK71jaO0wDT5PtEIUcxlafDJJ4u2KQwmYQIsUnYEC/5hln2jLOLdkUi5uin8f7rYrL8pp+TL4N0kB3xMrwymsyjBuQ1KhQBX2+C+eilyLLj+VD5T65Rg/0tkqjZtYjaKt4Bqq64BQ9VyIcj5AylAzeoytRL1UUAeVlCYVeMi5XjE1DIOvHxS/ml0Hq2lzI+6vbcP7bmSqnENWPC2OPse6x84Eka1AMo1tF35pROC7hHLuilCRy5j8DREhJsa1/8+O3gEtgojtpPC1LKObeQNebpiXHN4+suJ+eWY4pM5GTzJuQ5+vjyhDk+g1BPJfD1j6tSU2ixG7FdG2vceWDl249TEGEQvwN4Qva40ATfAw4WXG67WucH3h9+CI+iCt6fFI6gnKCc2juyWJpMaTIeBw==

On Wed, Sep 05, 2018 at 10:21:20AM +0200, Théo Zimmermann wrote:
> You may also install the (still existing) coq-ssreflect package and do
> "From mathcomp Require Import ssreflect." in which case it will change
> these options for you (but also a few others).

The package is nowadays called coq-mathcomp-ssreflect and the easy entry
point is

From mathcomp Require Import all_ssreflect.

Best,
--
Enrico Tassi

[Coq-Club] Using Ssreflect in Coq, Frédéric Blanqui, 09/05/2018
- Re: [Coq-Club] Using Ssreflect in Coq, Théo Zimmermann, 09/05/2018
  - Re: [Coq-Club] Using Ssreflect in Coq, Frédéric Blanqui, 09/05/2018
  - Re: [Coq-Club] Using Ssreflect in Coq, Enrico Tassi, 09/05/2018