The Coq mailing list

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

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.