From 46b9480a717d5ca78e354fa843f39eed87cb7b15 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:08:00 +0200
Subject: [refman] Rename num to natural

---
 doc/sphinx/language/extensions/match.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/language/extensions')

diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 182f599a29..c36b9deef3 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -879,7 +879,7 @@ generated expression and the original.
 Here is a summary of the error messages corresponding to each
 situation:
 
-.. exn:: The constructor @ident expects @num arguments.
+.. exn:: The constructor @ident expects @natural arguments.
          The variable ident is bound several times in pattern term
          Found a constructor of inductive type term while a constructor of term is expected
 
@@ -890,8 +890,8 @@ situation:
 
    The pattern matching is not exhaustive.
 
-.. exn:: The elimination predicate term should be of arity @num (for non \
-         dependent case) or @num (for dependent case).
+.. exn:: The elimination predicate term should be of arity @natural (for non \
+         dependent case) or @natural (for dependent case).
 
    The elimination predicate provided to match has not the expected arity.
 
-- 
cgit v1.2.3