From 0be7f92624494b00cf114914cb04a7443f15746f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 18 Jun 2018 11:47:11 +0200 Subject: Fix #7829: Spurious documentation failures. We split a Require Import in two to avoid reaching the timeout. --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'doc') 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. -- cgit v1.2.3