The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Thank you Théo. Perhaps it would be good to add this in the doc. Best, Frédéric.

Le 05/09/2018 à 10:21, Théo Zimmermann a écrit :

Hello,

"From Coq Require Import ssreflect." is a one-line command to use SSReflect. The rest are just recommendations of the SSReflect authors that you are perfectly allowed to ignore.

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).

Théo

Le mer. 5 sept. 2018 à 10:17, Frédéric Blanqui <frederic.blanqui AT inria.fr> a écrit :

Hello.

In https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=ssreflect#usage, it is written:

"All in all, this corresponds to working in the following context:

From Coq Require Import ssreflect ssrfun ssrbool.

Set Implicit Arguments.

Unset Strict Implicit.

Unset Printing Implicit Defensive."

Is this all we have to write before using Ssreflect? Isn't there a one-line command?

Frédéric.