From d5eb564a1ae46409e90a2c6bd6af5b77aa37773e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2020 20:24:46 +0200
Subject: Adding a wit_natural standard argument.

---
 plugins/cc/g_congruence.mlg | 4 ++--
 plugins/ltac/tacinterp.ml   | 3 +++
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg
index 3920e3da75..2c91901477 100644
--- a/plugins/cc/g_congruence.mlg
+++ b/plugins/cc/g_congruence.mlg
@@ -22,9 +22,9 @@ DECLARE PLUGIN "cc_plugin"
 
 TACTIC EXTEND cc
 | [ "congruence" ] -> { congruence_tac 1000 [] }
-| [ "congruence" integer(n) ] -> { congruence_tac n [] }
+| [ "congruence" natural(n) ] -> { congruence_tac n [] }
 | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l }
- |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
+| [ "congruence" natural(n) "with" ne_constr_list(l) ] ->
    { congruence_tac n l }
 END
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 88480194c8..2258201c22 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2027,6 +2027,9 @@ let () =
 let () =
   declare_uniform wit_int
 
+let () =
+  declare_uniform wit_nat
+
 let () =
   declare_uniform wit_bool
 
-- 
cgit v1.2.3