Imported Upstream version 8.4~betaupstream/8.4_beta

6 files changed, 117 insertions, 130 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index ae3afff4..bd2285bb 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,13 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: ascii_syntax.ml 12406 2009-10-21 15:12:52Z soubiran $ i*)
-
 open Pp
 open Util
 open Names
 open Pcoq
-open Rawterm
+open Glob_term
 open Topconstr
 open Libnames
 open Coqlib
@@ -41,9 +39,9 @@ let interp_ascii dloc p =
   let rec aux n p =
      if n = 0 then [] else
      let mp = p mod 2 in
-     RRef (dloc,if mp = 0 then glob_false else glob_true)
+     GRef (dloc,if mp = 0 then glob_false else glob_true)
      :: (aux (n-1) (p/2)) in
-  RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
+  GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
 
 let interp_ascii_string dloc s =
   let p =
@@ -59,12 +57,12 @@ let interp_ascii_string dloc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when n = 0 -> 0
-    | RRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | 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)
     | _ -> raise Non_closed_ascii in
   try
     let rec aux = function
-    | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+    | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -80,4 +78,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
+    ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 7b92a92f..446ae522 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nat_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
@@ -16,7 +14,7 @@ open Pp
 open Util
 open Names
 open Coqlib
-open Rawterm
+open Glob_term
 open Libnames
 open Bigint
 open Coqlib
@@ -38,11 +36,11 @@ let nat_of_int dloc n =
 	   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 = RRef (dloc, glob_O) in
-      let ref_S = RRef (dloc, glob_S) in
+      let ref_O = GRef (dloc, glob_O) in
+      let ref_S = GRef (dloc, glob_S) in
       let rec mk_nat acc n =
 	if n <> zero then
-	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
+	  mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
@@ -58,8 +56,8 @@ let nat_of_int dloc n =
 exception Non_closed_number
 
 let rec int_of_nat = function
-  | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
-  | RRef (_,z) when z = glob_O -> zero
+  | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
+  | GRef (_,z) when z = glob_O -> zero
   | _ -> raise Non_closed_number
 
 let uninterp_nat p =
@@ -75,4 +73,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,["Coq";"Init";"Datatypes"])
     nat_of_int
-    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true)
+    ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index a540a7d0..19a3c899 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -1,18 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: numbers_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
 open Libnames
-open Rawterm
+open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
@@ -48,7 +46,7 @@ let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)
 
 let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ]
 let bigN_path = make_path (bigN_module@["BigN"]) "t"
-let bigN_t = make_mind_mpdot bigN_module "BigN" "t_"
+let bigN_t = make_mind_mpdot bigN_module "BigN" "t'"
 let bigN_scope = "bigN_scope"
 
 (* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *)
@@ -100,9 +98,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 = RRef (dloc, int31_construct) in
-  let ref_0 = RRef (dloc, int31_0) in
-  let ref_1 = RRef (dloc, int31_1) in
+  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 rec args counter n =
     if counter <= 0 then
       []
@@ -110,7 +108,7 @@ let int31_of_pos_bigint dloc n =
       let (q,r) = div2_with_rest n in
 	(if r then ref_1 else ref_0)::(args (counter-1) q)
   in
-  RApp (dloc, ref_construct, List.rev (args 31 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.")
@@ -127,12 +125,12 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> cur
-      | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
-      | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 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))
       | _ -> raise Non_closed
   in
   function
-  | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero
+  | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
 let uninterp_int31 i =
@@ -145,7 +143,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([RRef (Util.dummy_loc, int31_construct)],
+  ([GRef (Util.dummy_loc, int31_construct)],
    uninterp_int31,
    true)
 
@@ -176,24 +174,24 @@ let height bi =
 
 (* n must be a non-negative integer (from bigint.ml) *)
 let word_of_pos_bigint dloc hght n =
-  let ref_W0 = RRef (dloc, zn2z_W0) in
-  let ref_WW = RRef (dloc, zn2z_WW) in
+  let ref_W0 = GRef (dloc, zn2z_W0) in
+  let ref_WW = GRef (dloc, zn2z_WW) in
   let rec decomp hgt n =
     if is_neg_or_zero hgt then
       int31_of_pos_bigint dloc n
     else if equal n zero then
-      RApp (dloc, ref_W0, [RHole (dloc, Evd.InternalHole)])
+      GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)])
     else
       let (h,l) = split_at hgt n in
-      RApp (dloc, ref_WW, [RHole (dloc, Evd.InternalHole);
+      GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole);
 			   decomp (sub_1 hgt) h;
 			   decomp (sub_1 hgt) l])
   in
   decomp hght n
 
 let bigN_of_pos_bigint dloc n =
-  let ref_constructor i = RRef (dloc, bigN_constructor i) in
-  let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then
+  let ref_constructor i = GRef (dloc, bigN_constructor i) in
+  let result h word = GApp (dloc, ref_constructor h, if less_than h n_inlined then
 				                       [word]
 			                             else
 				                      [Nat_syntax.nat_of_int dloc (sub h n_inlined);
@@ -217,7 +215,7 @@ let interp_bigN dloc n =
 let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+    | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
 	                                  let hleft = get_height lft in
 					  let hright = get_height rght in
 					  add_1
@@ -229,8 +227,8 @@ let bigint_of_word =
   in
   let rec transform hght rc =
     match rc with
-    | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero
-    | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in
+    | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
+    | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in
 	                                                add (mult (rank new_hght)
                                                           (transform (new_hght) lft))
 	                                            (transform (new_hght) rght)
@@ -242,8 +240,8 @@ let bigint_of_word =
 
 let bigint_of_bigN rc =
   match rc with
-  | RApp (_,_,[one_arg]) -> bigint_of_word one_arg
-  | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
+  | GApp (_,_,[one_arg]) -> bigint_of_word one_arg
+  | GApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
   | _ -> raise Non_closed
 
 let uninterp_bigN rc =
@@ -259,7 +257,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if less_than i (add_1 n_inlined) then
-      RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
+      GRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
     else
       []
   in
@@ -276,17 +274,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
 
 (*** Parsing for bigZ in digital notation ***)
 let interp_bigZ dloc n =
-  let ref_pos = RRef (dloc, bigZ_pos) in
-  let ref_neg = RRef (dloc, bigZ_neg) in
+  let ref_pos = GRef (dloc, bigZ_pos) in
+  let ref_neg = GRef (dloc, bigZ_neg) in
   if is_pos_or_zero n then
-    RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
+    GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
   else
-    RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
+    GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
-  | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
-  | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg ->
+  | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
+  | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
       let opp_val = bigint_of_bigN one_arg in
       if equal opp_val zero then
 	raise Non_closed
@@ -305,19 +303,19 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([RRef (Util.dummy_loc, bigZ_pos);
-    RRef (Util.dummy_loc, bigZ_neg)],
+  ([GRef (Util.dummy_loc, bigZ_pos);
+    GRef (Util.dummy_loc, bigZ_neg)],
    uninterp_bigZ,
    true)
 
 (*** Parsing for bigQ in digital notation ***)
 let interp_bigQ dloc n =
-  let ref_z = RRef (dloc, bigQ_z) in
-  RApp (dloc, ref_z, [interp_bigZ dloc n])
+  let ref_z = GRef (dloc, bigQ_z) in
+  GApp (dloc, ref_z, [interp_bigZ dloc n])
 
 let uninterp_bigQ rc =
   try match rc with
-    | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z ->
+    | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
 	Some (bigint_of_bigZ one_arg)
     | _ -> None (* we don't pretty-print yet fractions *)
   with Non_closed -> None
@@ -326,5 +324,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+  ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 43e79c82..b9c0bcd6 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: r_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pp
 open Util
 open Names
@@ -22,7 +20,7 @@ exception Non_closed_number
 (**********************************************************************)
 
 open Libnames
-open Rawterm
+open Glob_term
 open Bigint
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
@@ -48,24 +46,24 @@ let four = mult_2 two
 
 (* Unary representation of strictly positive numbers *)
 let rec small_r dloc n =
-  if equal one n then RRef (dloc, glob_R1)
-  else RApp(dloc,RRef (dloc,glob_Rplus),
-            [RRef (dloc, glob_R1);small_r dloc (sub_1 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)])
 
 let r_of_posint dloc n =
-  let r1 = RRef (dloc, glob_R1) in
+  let r1 = GRef (dloc, glob_R1) 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 = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
-      if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
-  if n <> zero then r_of_pos n else RRef(dloc,glob_R0)
+      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 r_of_int dloc z =
   if is_strictly_neg z then
-    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
+    GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
   else
     r_of_posint dloc z
 
@@ -77,33 +75,33 @@ let bignat_of_r =
 (* for numbers > 1 *)
 let rec bignat_of_pos = function
   (* 1+1 *)
-  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
+  | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)])
       when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
   (* 1+(1+1) *)
-  | RApp (_,RRef (_,p1), [RRef (_,o1);
-      RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
+  | 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
   (* (1+1)*b *)
-  | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
+  | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult ->
       if bignat_of_pos a <> two then raise Non_closed_number;
       mult_2 (bignat_of_pos b)
   (* 1+(1+1)*b *)
-  | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;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;
         add_1 (mult_2 (bignat_of_pos b))
   | _ -> raise Non_closed_number
 in
 let bignat_of_r = function
-  | RRef (_,a) when a = glob_R0 -> zero
-  | RRef (_,a) when a = glob_R1 -> one
+  | GRef (_,a) when a = glob_R0 -> zero
+  | GRef (_,a) when a = glob_R1 -> one
   | r -> bignat_of_pos r
 in
 bignat_of_r
 
 let bigint_of_r = function
-  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp ->
+  | GApp (_,GRef (_,o), [a]) when o = glob_Ropp ->
       let n = bignat_of_r a in
       if n = zero then raise Non_closed_number;
       neg n
@@ -118,8 +116,8 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
-    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);
-    RRef(dummy_loc,glob_R1)],
+  ([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)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 534605c8..d670f602 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: string_syntax.ml 12337 2009-09-17 15:58:14Z glondu $ i*)
-
 open Pp
 open Util
 open Names
@@ -15,7 +13,7 @@ open Pcoq
 open Libnames
 open Topconstr
 open Ascii_syntax
-open Rawterm
+open Glob_term
 open Coqlib
 
 exception Non_closed_string
@@ -39,8 +37,8 @@ open Lazy
 let interp_string dloc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then RRef (dloc, force glob_EmptyString) else
-     RApp (dloc,RRef (dloc, force glob_String),
+     if n = le then GRef (dloc, force glob_EmptyString) else
+     GApp (dloc,GRef (dloc, force glob_String),
        [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -48,11 +46,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | RApp (_,RRef (_,k),[a;s]) when k = force glob_String ->
+    | GApp (_,GRef (_,k),[a;s]) when k = force glob_String ->
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | RRef (_,z) when z = force glob_EmptyString ->
+    | GRef (_,z) when z = force glob_EmptyString ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -64,6 +62,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([RRef (dummy_loc,static_glob_String);
-      RRef (dummy_loc,static_glob_EmptyString)],
+    ([GRef (dummy_loc,static_glob_String);
+      GRef (dummy_loc,static_glob_EmptyString)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index e6dcc35e..f8bce8f7 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: z_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pcoq
 open Pp
 open Util
@@ -23,18 +21,19 @@ exception Non_closed_number
 (**********************************************************************)
 
 open Libnames
-open Rawterm
+open Glob_term
+
+let binnums = ["Coq";"Numbers";"BinNums"]
+
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let positive_module = ["Coq";"NArith";"BinPos"]
 let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 
-let positive_path = make_path positive_module "positive"
+let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
 let make_kn dir id = Libnames.encode_mind dir id
 
-let positive_kn =
-  make_kn (make_dir positive_module) (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)
@@ -44,13 +43,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat dloc x =
-  let ref_xI = RRef (dloc, glob_xI) in
-  let ref_xH = RRef (dloc, glob_xH) in
-  let ref_xO = RRef (dloc, glob_xO) in
+  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 rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
-      | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q])
+      | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
+      | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -68,9 +67,9 @@ let interp_positive dloc n =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
-  | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | RRef (_, a) when a = glob_xH -> Bigint.one
+  | 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
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
@@ -84,11 +83,11 @@ let uninterp_positive p =
 (************************************************************************)
 
 let _ = Notation.declare_numeral_interpreter "positive_scope"
-  (positive_path,positive_module)
+  (positive_path,binnums)
   interp_positive
-  ([RRef (dummy_loc, glob_xI);
-    RRef (dummy_loc, glob_xO);
-    RRef (dummy_loc, glob_xH)],
+  ([GRef (dummy_loc, glob_xI);
+    GRef (dummy_loc, glob_xO);
+    GRef (dummy_loc, glob_xH)],
    uninterp_positive,
    true)
 
@@ -96,21 +95,20 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let binnat_module = ["Coq";"NArith";"BinNat"]
-let n_kn = make_kn (make_dir binnat_module) (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)
 let glob_N0 = ConstructRef path_of_N0
 let glob_Npos = ConstructRef path_of_Npos
 
-let n_path = make_path binnat_module "N"
+let n_path = make_path binnums "N"
 
 let n_of_binnat dloc pos_or_neg n =
   if n <> zero then
-    RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n])
+    GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
   else
-    RRef (dloc, glob_N0)
+    GRef (dloc, glob_N0)
 
 let error_negative dloc =
   user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
@@ -124,8 +122,8 @@ let n_of_int dloc n =
 (**********************************************************************)
 
 let bignat_of_n = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
-  | RRef (_, a) when a = glob_N0 -> Bigint.zero
+  | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
+  | GRef (_, a) when a = glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_n p =
@@ -136,10 +134,10 @@ let uninterp_n p =
 (* Declaring interpreters and uninterpreters for N *)
 
 let _ = Notation.declare_numeral_interpreter "N_scope"
-  (n_path,binnat_module)
+  (n_path,binnums)
   n_of_int
-  ([RRef (dummy_loc, glob_N0);
-    RRef (dummy_loc, glob_Npos)],
+  ([GRef (dummy_loc, glob_N0);
+    GRef (dummy_loc, glob_Npos)],
   uninterp_n,
   true)
 
@@ -147,9 +145,8 @@ let _ = Notation.declare_numeral_interpreter "N_scope"
 (* Parsing Z via scopes                                               *)
 (**********************************************************************)
 
-let binint_module = ["Coq";"ZArith";"BinInt"]
-let z_path = make_path binint_module "Z"
-let z_kn = make_kn (make_dir binint_module) (id_of_string "Z")
+let z_path = make_path binnums "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)
@@ -162,18 +159,18 @@ let z_of_int dloc n =
   if n <> zero then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
+    GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
   else
-    RRef (dloc, glob_ZERO)
+    GRef (dloc, glob_ZERO)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_z = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
-  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | RRef (_, a) when a = glob_ZERO -> Bigint.zero
+  | 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
   | _ -> raise Non_closed_number
 
 let uninterp_z p =
@@ -185,10 +182,10 @@ let uninterp_z p =
 (* Declaring interpreters and uninterpreters for Z *)
 
 let _ = Notation.declare_numeral_interpreter "Z_scope"
-  (z_path,binint_module)
+  (z_path,binnums)
   z_of_int
-  ([RRef (dummy_loc, glob_ZERO);
-    RRef (dummy_loc, glob_POS);
-    RRef (dummy_loc, glob_NEG)],
+  ([GRef (dummy_loc, glob_ZERO);
+    GRef (dummy_loc, glob_POS);
+    GRef (dummy_loc, glob_NEG)],
   uninterp_z,
   true)