Imported Upstream version 8.5~beta1+dfsg

6 files changed, 134 insertions, 153 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index bd2285bb..67c9dd0a 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -7,20 +7,18 @@
 (***********************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
-open Pcoq
 open Glob_term
-open Topconstr
-open Libnames
+open Globnames
 open Coqlib
-open Bigint
 
 exception Non_closed_ascii
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_kn dir id = Libnames.encode_mind (make_dir dir) (id_of_string id)
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
 
@@ -37,17 +35,17 @@ open Lazy
 
 let interp_ascii dloc p =
   let rec aux n p =
-     if n = 0 then [] else
+     if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if mp = 0 then glob_false else glob_true)
+     GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None)
      :: (aux (n-1) (p/2)) in
-  GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
+  GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
 
 let interp_ascii_string dloc s =
   let p =
-    if String.length s = 1 then int_of_char s.[0]
+    if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
-      if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2]
+      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
       then int_of_string s
       else
 	user_err_loc (dloc,"interp_ascii_string",
@@ -56,13 +54,13 @@ let interp_ascii_string dloc s =
 
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
-    | [] when n = 0 -> 0
-    | GRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | [] when Int.equal n 0 -> 0
+    | GRef (_,k,_)::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
-    let rec aux = function
-    | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+    let aux = function
+    | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -78,4 +76,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,None)], uninterp_ascii_string, true)
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)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 5d43b353..b990c0d2 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_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,18 +9,19 @@
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
-open Libnames
+open Names
+open Globnames
 open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
-let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id)
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
-let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
-let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
+let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
+let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
-  let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname)
+  let mp = MPdot (MPfile (make_dir dir), Label.make modname)
   in make_mind mp id
 
 
@@ -82,9 +83,9 @@ exception Non_closed
 (* parses a *non-negative* integer (from bigint.ml) into an int31
    wraps modulo 2^31 *)
 let int31_of_pos_bigint dloc n =
-  let ref_construct = GRef (dloc, int31_construct) in
-  let ref_0 = GRef (dloc, int31_0) in
-  let ref_1 = GRef (dloc, int31_1) in
+  let ref_construct = GRef (dloc, int31_construct, None) in
+  let ref_0 = GRef (dloc, int31_0, None) in
+  let ref_1 = GRef (dloc, int31_1, None) in
   let rec args counter n =
     if counter <= 0 then
       []
@@ -95,7 +96,7 @@ let int31_of_pos_bigint dloc n =
   GApp (dloc, ref_construct, List.rev (args 31 n))
 
 let error_negative dloc =
-  Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
+  Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
 
 let interp_int31 dloc n =
   if is_pos_or_zero n then
@@ -109,12 +110,12 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> cur
-      | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
-      | (GRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
+      | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+      | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
   function
-  | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
+  | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
 let uninterp_int31 i =
@@ -127,7 +128,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([GRef (Util.dummy_loc, int31_construct)],
+  ([GRef (Loc.ghost, int31_construct, None)],
    uninterp_int31,
    true)
 
@@ -158,16 +159,16 @@ let height bi =
 
 (* n must be a non-negative integer (from bigint.ml) *)
 let word_of_pos_bigint dloc hght n =
-  let ref_W0 = GRef (dloc, zn2z_W0) in
-  let ref_WW = GRef (dloc, zn2z_WW) in
+  let ref_W0 = GRef (dloc, zn2z_W0, None) in
+  let ref_WW = GRef (dloc, zn2z_WW, None) in
   let rec decomp hgt n =
     if hgt <= 0 then
       int31_of_pos_bigint dloc n
     else if equal n zero then
-      GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)])
+      GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
     else
       let (h,l) = split_at hgt n in
-      GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole);
+      GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
 			   decomp (hgt-1) h;
 			   decomp (hgt-1) l])
   in
@@ -175,7 +176,7 @@ let word_of_pos_bigint dloc hght n =
 
 let bigN_of_pos_bigint dloc n =
   let h = height n in
-  let ref_constructor = GRef (dloc, bigN_constructor h) in
+  let ref_constructor = GRef (dloc, bigN_constructor h, None) in
   let word = word_of_pos_bigint dloc h n in
   let args =
     if h < n_inlined then [word]
@@ -184,7 +185,7 @@ let bigN_of_pos_bigint dloc n =
   GApp (dloc, ref_constructor, args)
 
 let bigN_error_negative dloc =
-  Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
+  Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
 
 let interp_bigN dloc n =
   if is_pos_or_zero n then
@@ -198,14 +199,14 @@ let interp_bigN dloc n =
 let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+    | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW ->
       1+max (get_height lft) (get_height rght)
     | _ -> 0
   in
   let rec transform hght rc =
     match rc with
-    | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
-    | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW->
+    | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero
+    | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW->
       let new_hght = hght-1 in
       add (mult (rank new_hght)
              (transform new_hght lft))
@@ -235,7 +236,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if i < n_inlined+1 then
-      GRef (Util.dummy_loc, bigN_constructor i)::(build (i+1))
+      GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1))
     else
       []
   in
@@ -252,8 +253,8 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
 
 (*** Parsing for bigZ in digital notation ***)
 let interp_bigZ dloc n =
-  let ref_pos = GRef (dloc, bigZ_pos) in
-  let ref_neg = GRef (dloc, bigZ_neg) in
+  let ref_pos = GRef (dloc, bigZ_pos, None) in
+  let ref_neg = GRef (dloc, bigZ_neg, None) in
   if is_pos_or_zero n then
     GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
   else
@@ -261,8 +262,8 @@ let interp_bigZ dloc n =
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
-  | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
-  | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
+  | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+  | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg ->
       let opp_val = bigint_of_bigN one_arg in
       if equal opp_val zero then
 	raise Non_closed
@@ -281,19 +282,19 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([GRef (Util.dummy_loc, bigZ_pos);
-    GRef (Util.dummy_loc, bigZ_neg)],
+  ([GRef (Loc.ghost, bigZ_pos, None);
+    GRef (Loc.ghost, bigZ_neg, None)],
    uninterp_bigZ,
    true)
 
 (*** Parsing for bigQ in digital notation ***)
 let interp_bigQ dloc n =
-  let ref_z = GRef (dloc, bigQ_z) in
+  let ref_z = GRef (dloc, bigQ_z, None) in
   GApp (dloc, ref_z, [interp_bigZ dloc n])
 
 let uninterp_bigQ rc =
   try match rc with
-    | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
+    | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z ->
 	Some (bigint_of_bigZ one_arg)
     | _ -> None (* we don't pretty-print yet fractions *)
   with Non_closed -> None
@@ -302,5 +303,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+  ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 79a4d8e6..2c195755 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -1,17 +1,14 @@
 (************************************************************************)
 (*  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        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Names
-open Pcoq
-open Topconstr
-open Libnames
+open Globnames
 
 exception Non_closed_number
 
@@ -19,18 +16,17 @@ exception Non_closed_number
 (* Parsing R via scopes                                               *)
 (**********************************************************************)
 
-open Libnames
 open Glob_term
 open Bigint
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
-let make_path dir id = Libnames.make_path dir (id_of_string id)
+let make_path dir id = Libnames.make_path dir (Id.of_string id)
 
 let r_path = make_path rdefinitions "R"
 
 (* TODO: temporary hack *)
-let make_path dir id = Libnames.encode_con dir (id_of_string id)
+let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 
 let r_kn = make_path rdefinitions "R"
 let glob_R = ConstRef r_kn
@@ -46,24 +42,24 @@ let four = mult_2 two
 
 (* Unary representation of strictly positive numbers *)
 let rec small_r dloc n =
-  if equal one n then GRef (dloc, glob_R1)
-  else GApp(dloc,GRef (dloc,glob_Rplus),
-            [GRef (dloc, glob_R1);small_r dloc (sub_1 n)])
+  if equal one n then GRef (dloc, glob_R1, None)
+  else GApp(dloc,GRef (dloc,glob_Rplus, None),
+            [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)])
 
 let r_of_posint dloc n =
-  let r1 = GRef (dloc, glob_R1) in
+  let r1 = GRef (dloc, glob_R1, None) in
   let r2 = small_r dloc two in
   let rec r_of_pos n =
     if less_than n four then small_r dloc n
     else
       let (q,r) = div2_with_rest n in
-      let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
-      if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in
-  if n <> zero then r_of_pos n else GRef(dloc,glob_R0)
+      let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in
+      if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in
+  if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None)
 
 let r_of_int dloc z =
   if is_strictly_neg z then
-    GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
+    GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)])
   else
     r_of_posint dloc z
 
@@ -75,35 +71,35 @@ let bignat_of_r =
 (* for numbers > 1 *)
 let rec bignat_of_pos = function
   (* 1+1 *)
-  | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)])
-      when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
+  | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)])
+      when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two
   (* 1+(1+1) *)
-  | GApp (_,GRef (_,p1), [GRef (_,o1);
-      GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])])
-      when p1 = glob_Rplus & p2 = glob_Rplus &
-           o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three
+  | GApp (_,GRef (_,p1,_), [GRef (_,o1,_);
+      GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])])
+      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus &&
+           Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three
   (* (1+1)*b *)
-  | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
+  | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult ->
+      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
       mult_2 (bignat_of_pos b)
   (* 1+(1+1)*b *)
-  | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])])
-      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
+  | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])])
+      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1  ->
+      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
         add_1 (mult_2 (bignat_of_pos b))
   | _ -> raise Non_closed_number
 in
 let bignat_of_r = function
-  | GRef (_,a) when a = glob_R0 -> zero
-  | GRef (_,a) when a = glob_R1 -> one
+  | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero
+  | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one
   | r -> bignat_of_pos r
 in
 bignat_of_r
 
 let bigint_of_r = function
-  | GApp (_,GRef (_,o), [a]) when o = glob_Ropp ->
+  | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp ->
       let n = bignat_of_r a in
-      if n = zero then raise Non_closed_number;
+      if Bigint.equal n zero then raise Non_closed_number;
       neg n
   | a -> bignat_of_r a
 
@@ -113,11 +109,12 @@ let uninterp_r p =
   with Non_closed_number ->
     None
 
+let mkGRef gr = GRef (Loc.ghost,gr,None)
+
 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)],
+  (List.map mkGRef 
+    [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index d670f602..2e696f39 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -6,12 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open Pp
-open Util
-open Names
-open Pcoq
-open Libnames
-open Topconstr
+open Globnames
 open Ascii_syntax
 open Glob_term
 open Coqlib
@@ -37,8 +32,8 @@ open Lazy
 let interp_string dloc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then GRef (dloc, force glob_EmptyString) else
-     GApp (dloc,GRef (dloc, force glob_String),
+     if n = le then GRef (dloc, force glob_EmptyString, None) else
+     GApp (dloc,GRef (dloc, force glob_String, None),
        [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -46,11 +41,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | GApp (_,GRef (_,k),[a;s]) when k = force glob_String ->
+    | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) ->
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | GRef (_,z) when z = force glob_EmptyString ->
+    | GRef (_,z,_) when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -62,6 +57,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,None);
+      GRef (Loc.ghost,static_glob_EmptyString,None)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 4025893d..e3721362 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -1,17 +1,15 @@
 (************************************************************************)
 (*  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        *)
 (************************************************************************)
 
-open Pcoq
 open Pp
+open Errors
 open Util
 open Names
-open Topconstr
-open Libnames
 open Bigint
 
 exception Non_closed_number
@@ -20,20 +18,20 @@ exception Non_closed_number
 (* Parsing positive via scopes                                        *)
 (**********************************************************************)
 
-open Libnames
+open Globnames
 open Glob_term
 
 let binnums = ["Coq";"Numbers";"BinNums"]
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_mind dir id
+let make_kn dir id = Globnames.encode_mind dir id
 
-let positive_kn = make_kn (make_dir binnums) (id_of_string "positive")
+let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
 let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
@@ -43,13 +41,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat dloc x =
-  let ref_xI = GRef (dloc, glob_xI) in
-  let ref_xH = GRef (dloc, glob_xH) in
-  let ref_xO = GRef (dloc, glob_xO) in
+  let ref_xI = GRef (dloc, glob_xI, None) in
+  let ref_xH = GRef (dloc, glob_xH, None) in
+  let ref_xO = GRef (dloc, glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
       | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
-      | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -67,9 +65,9 @@ let interp_positive dloc n =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (_, a) when a = glob_xH -> Bigint.one
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
@@ -85,9 +83,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, None);
+    GRef (Loc.ghost, glob_xO, None);
+    GRef (Loc.ghost, glob_xH, None)],
    uninterp_positive,
    true)
 
@@ -95,7 +93,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let n_kn = make_kn (make_dir binnums) (id_of_string "N")
+let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
 let glob_n = IndRef (n_kn,0)
 let path_of_N0 = ((n_kn,0),1)
 let path_of_Npos = ((n_kn,0),2)
@@ -105,10 +103,10 @@ let glob_Npos = ConstructRef path_of_Npos
 let n_path = make_path binnums "N"
 
 let n_of_binnat dloc pos_or_neg n =
-  if n <> zero then
-    GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
+  if not (Bigint.equal n zero) then
+    GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n])
   else
-    GRef (dloc, glob_N0)
+    GRef (dloc, glob_N0, None)
 
 let error_negative dloc =
   user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
@@ -122,8 +120,8 @@ let n_of_int dloc n =
 (**********************************************************************)
 
 let bignat_of_n = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
-  | GRef (_, a) when a = glob_N0 -> Bigint.zero
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+  | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_n p =
@@ -136,8 +134,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, None);
+    GRef (Loc.ghost, glob_Npos, None)],
   uninterp_n,
   true)
 
@@ -146,7 +144,7 @@ let _ = Notation.declare_numeral_interpreter "N_scope"
 (**********************************************************************)
 
 let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (id_of_string "Z")
+let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
 let glob_z = IndRef (z_kn,0)
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
@@ -156,21 +154,21 @@ let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
 let z_of_int dloc n =
-  if n <> zero then
+  if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
+    GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n])
   else
-    GRef (dloc, glob_ZERO)
+    GRef (dloc, glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_z = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
-  | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (_, a) when a = glob_ZERO -> Bigint.zero
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_z p =
@@ -184,8 +182,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, None);
+    GRef (Loc.ghost, glob_POS, None);
+    GRef (Loc.ghost, glob_NEG, None)],
   uninterp_z,
   true)