diff options
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 26 |
1 files changed, 9 insertions, 17 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 2899f17f..0f280aad 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,19 +9,11 @@ (* This file defines the printer for natural numbers in [nat] *) (*i*) -open Pcoq -open Pp -open Util -open Names -open Coqlib open Glob_term -open Libnames open Bigint open Coqlib -open Notation open Pp -open Util -open Names +open Errors (*i*) (**********************************************************************) @@ -33,13 +25,13 @@ let threshold = of_int 5000 let nat_of_int dloc n = if is_pos_or_zero n then begin if less_than threshold n then - Flags.if_warn msg_warning + msg_warning (strbrk "Stack overflow or segmentation fault happens when " ++ 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) @@ -58,8 +50,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) - | GRef (_,z) when 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 = @@ -73,6 +65,6 @@ let uninterp_nat p = let _ = Notation.declare_numeral_interpreter "nat_scope" - (nat_path,["Coq";"Init";"Datatypes"]) + (nat_path,datatypes_module_name) nat_of_int - ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true) + ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) |