diff options
Diffstat (limited to 'plugins/syntax/numbers_syntax.ml')
| -rw-r--r-- | plugins/syntax/numbers_syntax.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index fe9f1319e..57cb2f897 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "numbers_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint @@ -180,7 +184,7 @@ let bigN_of_pos_bigint dloc n = let word = word_of_pos_bigint dloc h n in let args = if h < n_inlined then [word] - else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] + else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] in GApp (dloc, ref_constructor, args) |