From 5d1f7461f74f727d0394e904c3ee820134b22c64 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 30 Oct 2019 17:08:51 +0100
Subject: Use explicit match as suggested by Clément.

---
 doc/sphinx/language/cic.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index ef896b6f03..9e4210793e 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1067,7 +1067,8 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: all
 
-      Definition I_not_I '(not_I_I not_I : I) : ~ I := not_I.
+      Definition I_not_I : I -> ~ I := fun i =>
+        match i with not_I_I not_I => not_I end.
 
    .. coqtop:: in
 
-- 
cgit v1.2.3