diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-19 08:25:00 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-19 08:25:00 +0200 |
| commit | f0ae8e82ea53ce72ddac1fb8f7f40fd1beacf787 (patch) | |
| tree | f2755660245d87bab447f0f63e50f544e840f0b5 | |
| parent | 26d2171060daf642008fd2430c8f78b8f7b9c43c (diff) | |
| parent | 0be7f92624494b00cf114914cb04a7443f15746f (diff) | |
Merge PR #7856: Fix #7829: Spurious documentation failures.
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b2009657..1c554acdb 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3657,7 +3657,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. coqtop:: reset - From Coq Require Import ssreflect ssrfun ssrbool List. + From Coq Require Import ssreflect ssrfun ssrbool. + From Coq Require Import List. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. |