Skip to content

Commit

Permalink
bignums_syntax: avoid depending on Nat_syntax_plugin
Browse files Browse the repository at this point in the history
 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 b3ae597 (bad merge ?).
  • Loading branch information
letouzey committed Mar 12, 2018
1 parent 8675e53 commit 1cafe43
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion bignums_syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit 1cafe43

Please sign in to comment.