Change of nomenclature: rawconstr -> glob_constr

There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.

In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.

The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.

This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):

perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 94 insertions, 94 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 79e1a6eb2..50498f0f4 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -39,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 =
@@ -57,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
@@ -78,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 b673fdb9d..3d8860be4 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -36,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
@@ -56,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 =
@@ -73,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 2a0425dca..892a5595a 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -98,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
       []
@@ -108,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.")
@@ -125,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 =
@@ -143,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)
 
@@ -174,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);
@@ -215,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
@@ -227,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)
@@ -240,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 =
@@ -257,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
@@ -274,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
@@ -303,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
@@ -324,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 7f093ae95..fc953e5e5 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -46,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
 
@@ -75,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
@@ -116,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 cb2b16858..61643881e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -37,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
 
@@ -46,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
@@ -62,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 fb8de1f92..81588bced 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -42,13 +42,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
@@ -66,9 +66,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,9 +84,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,positive_module)
   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)
 
@@ -106,9 +106,9 @@ let n_path = make_path binnat_module "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\".")
@@ -122,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,8 +136,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnat_module)
   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)
 
@@ -160,18 +160,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,8 +185,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binint_module)
   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)