From 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 8 Sep 2020 10:41:03 +0200
Subject: Turn integer into natural in several mlgs

Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
---
 doc/sphinx/proof-engine/ltac.rst  | 2 +-
 doc/sphinx/proof-engine/ltac2.rst | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2a102adfcc..f18569c7fd 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -876,7 +876,7 @@ Print/identity tactic: idtac
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 
-.. tacn:: idtac {* {| @ident | @string | @integer } }
+.. tacn:: idtac {* {| @ident | @string | @natural } }
    :name: idtac
 
    Leaves the proof unchanged and prints the given tokens. Strings and integers are printed
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b4f32c6cbb..773e393eb6 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1159,7 +1159,7 @@ Match on values
 Notations
 ---------
 
-.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @integer } := @ltac2_expr
+.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr
    :name: Ltac2 Notation
 
    .. todo seems like name maybe should use lident rather than ident, considering:
-- 
cgit v1.2.3