From 1cafe43151450d7a3f7a0b2c8036851900e3eab9 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 12 Mar 2018 16:44:05 +0100 Subject: [PATCH] bignums_syntax: avoid depending on Nat_syntax_plugin This makes bignums compatible with Coq PR #496 (about Numeral Notation), but is also ok (and even nicer) for current Coq master. Actually, the work has already been done some time ago, by embedding a local simplified version of nat_of_int just before. But the reference to Nat_syntax_plugin was erroneously reintroduced by b3ae5975 (bad merge ?). --- bignums_syntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bignums_syntax.ml b/bignums_syntax.ml index 51cd5d1..4fb7bb6 100644 --- a/bignums_syntax.ml +++ b/bignums_syntax.ml @@ -198,7 +198,7 @@ let bigN_of_pos_bigint ?loc n = let word = word_of_pos_bigint ?loc h n in let args = if h < n_inlined then [word] - else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word] + else [nat_of_int ?loc (h-n_inlined);word] in DAst.make ?loc @@ GApp (ref_constructor, args)