From 6b45f2d36929162cf92272bb60c2c245d9a0ead3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 22 Jun 2012 15:14:30 +0000
Subject: Added an indirection with respect to Loc in Compat. As many [open
 Compat] were closed (i.e. the only remaining ones are those of
 printing/parsing). Meanwhile, a simplified interface is provided in loc.mli.

This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/syntax/numbers_syntax.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

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

diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index b67cbb9343..97753951a1 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -144,7 +144,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([GRef (Pp.dummy_loc, int31_construct)],
+  ([GRef (Loc.ghost, int31_construct)],
    uninterp_int31,
    true)
 
@@ -258,7 +258,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if less_than i (add_1 n_inlined) then
-      GRef (Pp.dummy_loc, bigN_constructor i)::(build (add_1 i))
+      GRef (Loc.ghost, bigN_constructor i)::(build (add_1 i))
     else
       []
   in
@@ -304,8 +304,8 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([GRef (Pp.dummy_loc, bigZ_pos);
-    GRef (Pp.dummy_loc, bigZ_neg)],
+  ([GRef (Loc.ghost, bigZ_pos);
+    GRef (Loc.ghost, bigZ_neg)],
    uninterp_bigZ,
    true)
 
@@ -325,5 +325,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([GRef (Pp.dummy_loc, bigQ_z)], uninterp_bigQ,
+  ([GRef (Loc.ghost, bigQ_z)], uninterp_bigQ,
    true)
-- 
cgit v1.2.3