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

6 files changed, 20 insertions, 20 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index b2e2e5b19..17dd563f7 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -80,4 +80,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
+    ([GRef (Loc.ghost,static_glob_Ascii)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5a355b971..2fb8ce451 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -75,4 +75,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,["Coq";"Init";"Datatypes"])
     nat_of_int
-    ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true)
+    ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index b67cbb934..97753951a 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)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index f8161c52f..4e0a206dd 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -118,8 +118,8 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([GRef(dummy_loc,glob_Ropp);GRef(dummy_loc,glob_R0);
-    GRef(dummy_loc,glob_Rplus);GRef(dummy_loc,glob_Rmult);
-    GRef(dummy_loc,glob_R1)],
+  ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0);
+    GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult);
+    GRef(Loc.ghost,glob_R1)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index ac17492d2..7474a8b0e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -64,6 +64,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([GRef (dummy_loc,static_glob_String);
-      GRef (dummy_loc,static_glob_EmptyString)],
+    ([GRef (Loc.ghost,static_glob_String);
+      GRef (Loc.ghost,static_glob_EmptyString)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index a69ec9ed1..e461ea152 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -87,9 +87,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([GRef (dummy_loc, glob_xI);
-    GRef (dummy_loc, glob_xO);
-    GRef (dummy_loc, glob_xH)],
+  ([GRef (Loc.ghost, glob_xI);
+    GRef (Loc.ghost, glob_xO);
+    GRef (Loc.ghost, glob_xH)],
    uninterp_positive,
    true)
 
@@ -138,8 +138,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([GRef (dummy_loc, glob_N0);
-    GRef (dummy_loc, glob_Npos)],
+  ([GRef (Loc.ghost, glob_N0);
+    GRef (Loc.ghost, glob_Npos)],
   uninterp_n,
   true)
 
@@ -186,8 +186,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([GRef (dummy_loc, glob_ZERO);
-    GRef (dummy_loc, glob_POS);
-    GRef (dummy_loc, glob_NEG)],
+  ([GRef (Loc.ghost, glob_ZERO);
+    GRef (Loc.ghost, glob_POS);
+    GRef (Loc.ghost, glob_NEG)],
   uninterp_z,
   true)