Commit ab2b5816 authored by Ralf Jung's avatar Ralf Jung

turns out we can import with shorter names (and we actually already do that...

turns out we can import with shorter names (and we actually already do that frequently in "From Coq Import")
parent 35c154c4
From mathcomp.ssreflect Require Export ssreflect.
From mathcomp Require Export ssreflect.
From prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment