diff options
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c3dad0a10..bad099d4f 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -30,8 +30,8 @@ let nat_of_int dloc n = strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ strbrk "limits and on the command executed)."); - let ref_O = GRef (dloc, glob_O) in - let ref_S = GRef (dloc, glob_S) in + let ref_O = GRef (dloc, glob_O, None) in + let ref_S = GRef (dloc, glob_S, None) in let rec mk_nat acc n = if n <> zero then mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) @@ -50,8 +50,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | GApp (_,GRef (_,s),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) - | GRef (_,z) when Globnames.eq_gr z glob_O -> zero + | GApp (_,GRef (_,s,_),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | GRef (_,z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number let uninterp_nat p = @@ -67,4 +67,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true) + ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) |