diff options
| author | Maxime Dénès | 2017-05-25 11:16:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-25 11:16:35 +0200 |
| commit | f2fec63025d933f56dabf114a51720b1aae626c1 (patch) | |
| tree | 7f729302601fef48e6c59534a7904c7dfb92df2d /plugins/syntax/nat_syntax.ml | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
| parent | 94e783390ef9ad9d26a54add2287e0a3e58d1b70 (diff) | |
Merge PR#402: Uniform attribute handling in interfaces
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index ab262fea70..9a4cd6c254 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -33,21 +33,21 @@ let warn_large_nat = strbrk "may vary from 5000 to 70000 depending on your system " ++ strbrk "limits and on the command executed).") -let nat_of_int dloc n = +let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = GRef (dloc, glob_O, None) in - let ref_S = GRef (dloc, glob_S, None) in + let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) + mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in mk_nat ref_O n end else - user_err ~hdr:"nat_of_int" + user_err ?loc ~hdr:"nat_of_int" (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) @@ -55,10 +55,11 @@ 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 +let rec int_of_nat x = CAst.with_val (function + | GApp ({ CAst.v = 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 + ) x let uninterp_nat p = try @@ -73,4 +74,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) + ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true) |