From 6d85d5e825f19f3e2103273648d8c7976d115ec9 Mon Sep 17 00:00:00 2001
From: Matěj G
Date: Fri, 7 Sep 2018 18:21:20 +0200
Subject: Recover lost snippet

This snippet on pattern matching got lost in the process of migrating to Sphynx.---
 doc/sphinx/addendum/extended-pattern-matching.rst | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index f7fd4b9146..e507a224c6 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -407,12 +407,11 @@ length, by writing
 
 .. coqtop:: in
 
-   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
-    listn (n + m) :=
-     match l in listn n, l' return listn (n + m) with
-     | niln, x => x
-     | consn n' a y, x => consn (n' + m) a (concat n' y m x)
-     end.
+   Check (fun n (a b: listn n) =>
+    match a, b with
+    | niln, b0 => tt
+    | consn n' a y, bS => tt
+    end).
 
 we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`.
 
-- 
cgit v1.2.3