From 31c04ca25cbb9963d74060746ba57460d98acbfe Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Thu, 5 Apr 2018 14:55:59 +0200
Subject: Sphinx docs: clarify strict implicit arguments

---
 doc/sphinx/language/gallina-extensions.rst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 1d6c11b38d..9afeaced94 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1477,7 +1477,9 @@ For instance, the first argument of
 
 in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A`
 will always be inferable from the type :g:`list A` of the third argument of
-:g:`cons`. On the contrary, the second argument of a term of type
+:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one,
+since the first argument is exactly the type of the second argument.
+On the contrary, the second argument of a term of type
 ::
 
   forall P:nat->Prop, forall n:nat, P n -> ex nat P
-- 
cgit v1.2.3