Skip to content

Commit

Permalink
Merge pull request #86 from ppedrot/fix-bignums
Browse files Browse the repository at this point in the history
Fix compilation on Coq master.
  • Loading branch information
proux01 committed Feb 13, 2024
2 parents 9184704 + c5bde2b commit 3885b1a
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions plugin/bignums_syntax.ml
Expand Up @@ -198,15 +198,15 @@ let bigN_list_of_constructors =
let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) =
let open Notation in
register_bignumeral_interpretation uid (interp,uninterp);
{ pt_local = false;
enable_prim_token_interpretation { pt_local = false;
pt_scope = sc;
pt_interp_info = Uid uid;
pt_required = dir;
pt_refs = patl;
pt_in_match = b }

(* Actually declares the interpreter for bigN *)
let _ =
let () =
Notation.declare_scope bigN_scope;
declare_numeral_interpreter "bignums.bigN" bigN_scope
(bigN_path, bigN_module)
Expand Down Expand Up @@ -244,7 +244,7 @@ let uninterp_bigZ (AnyGlobConstr rc) =
None

(* Actually declares the interpreter for bigZ *)
let _ =
let () =
Notation.declare_scope bigZ_scope;
declare_numeral_interpreter "bignums.bigZ" bigZ_scope
(bigZ_path, bigZ_module)
Expand All @@ -266,7 +266,7 @@ let uninterp_bigQ (AnyGlobConstr rc) =
with Non_closed -> None

(* Actually declares the interpreter for bigQ *)
let _ =
let () =
Notation.declare_scope bigQ_scope;
declare_numeral_interpreter "bignums.bigQ" bigQ_scope
(bigQ_path, bigQ_module)
Expand Down

0 comments on commit 3885b1a

Please sign in to comment.