[Coq-Club] Using Ssreflect in Coq

[Frédéric Blanqui]

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:

FromCoqRequireImportssreflectssrfunssrbool.
Set Implicit Arguments.
UnsetStrictImplicit.
UnsetPrintingImplicitDefensive."

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

Frédéric.

[Théo Zimmermann]

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

Post by Frédéric Blanqui
Hello.
In
https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=ssreflect#usage,
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.

[Frédéric Blanqui]

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

Post by Théo Zimmermann
Hello,
"FromCoqRequireImportssreflect." 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
Hello.
In
https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=ssreflect#usage,
FromCoqRequireImportssreflectssrfunssrbool.
Set Implicit Arguments.
UnsetStrictImplicit.
UnsetPrintingImplicitDefensive."
Is this all we have to write before using Ssreflect? Isn't there a
one-line command?
Frédéric.

[Enrico Tassi]

Post by Théo Zimmermann
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,