diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-18 11:47:11 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-18 11:47:11 +0200 |
| commit | 0be7f92624494b00cf114914cb04a7443f15746f (patch) | |
| tree | 6978dbe6d7b251629faf85a81ac984e519386469 /doc | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Fix #7829: Spurious documentation failures.
We split a Require Import in two to avoid reaching the timeout.
Diffstat (limited to 'doc')
| -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. |