diff options
Diffstat (limited to 'plugins/syntax/int31_syntax.ml')
| -rw-r--r-- | plugins/syntax/int31_syntax.ml | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index 5529ea70..e34a401c 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -26,7 +26,7 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let make_mind mp id = Names.MutInd.make2 mp (Label.make id) @@ -96,10 +96,19 @@ let uninterp_int31 (AnyGlobConstr i) = with Non_closed -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + (* Actually declares the interpreter for int31 *) -let _ = Notation.declare_numeral_interpreter int31_scope - (int31_path, int31_module) - interp_int31 - ([DAst.make (GRef (int31_construct, None))], - uninterp_int31, - true) + +let _ = + register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = int31_scope; + pt_interp_info = Uid int31_scope; + pt_required = (int31_path,int31_module); + pt_refs = [int31_construct]; + pt_in_match = true } |