From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:23:53 +0100
Subject: [location] Switch glob_constr to Loc.located

---
 plugins/syntax/nat_syntax.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/syntax/nat_syntax.ml')

diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index ab262fea70..90d643b7f2 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -33,14 +33,14 @@ 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 = Loc.tag ~loc @@ GRef (glob_O, None) in
+      let ref_S = Loc.tag ~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 (Loc.tag ~loc @@ GApp (ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
@@ -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 = Loc.with_unloc (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
   | _ -> 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)
+    ([Loc.tag @@ GRef (glob_S,None); Loc.tag @@ GRef (glob_O,None)], uninterp_nat, true)
-- 
cgit v1.2.3