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

1 files changed, 6 insertions, 6 deletions

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)