diff options
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index b673fdb9d..3d8860be4 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -36,11 +36,11 @@ 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 = RRef (dloc, glob_O) in - let ref_S = RRef (dloc, glob_S) in + let ref_O = GRef (dloc, glob_O) in + let ref_S = GRef (dloc, glob_S) in let rec mk_nat acc n = if n <> zero then - mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n) + mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) else acc in @@ -56,8 +56,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) - | RRef (_,z) when z = glob_O -> zero + | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) + | GRef (_,z) when z = glob_O -> zero | _ -> raise Non_closed_number let uninterp_nat p = @@ -73,4 +73,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,["Coq";"Init";"Datatypes"]) nat_of_int - ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true) + ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true) |