Skip to content

Commit 6e7932a

Browse files
authored
Merge pull request #99 from SkySkimmer/module-is-known
Adapt to rocq-prover/rocq#20853 (rm add_known_module)
2 parents 9f98555 + 333cd27 commit 6e7932a

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

plugin/bignums_syntax.ml

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,6 @@
66
(* * GNU Lesser General Public License Version 2.1 *)
77
(************************************************************************)
88

9-
(* Poor's man DECLARE PLUGIN *)
10-
let __coq_plugin_name = "coq-bignums.plugin"
11-
let () = Mltop.add_known_module __coq_plugin_name
12-
139
(* digit-based syntax for int63, bigN bigZ and bigQ *)
1410

1511
open Names

0 commit comments

Comments
 (0)