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, 23 insertions, 23 deletions

diff --git a/interp/reserve.ml b/interp/reserve.ml
index 2d36f2409..9d20236b8 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -49,42 +49,42 @@ let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
 open Rawterm
 
 let rec unloc = function
-  | RVar (_,id) -> RVar (dummy_loc,id)
-  | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
-  | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
-  | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
-  | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
-  | RCases (_,sty,rtntypopt,tml,pl) ->
-      RCases (dummy_loc,sty,
+  | GVar (_,id) -> GVar (dummy_loc,id)
+  | GApp (_,g,args) -> GApp (dummy_loc,unloc g, List.map unloc args)
+  | GLambda (_,na,bk,ty,c) -> GLambda (dummy_loc,na,bk,unloc ty,unloc c)
+  | GProd (_,na,bk,ty,c) -> GProd (dummy_loc,na,bk,unloc ty,unloc c)
+  | GLetIn (_,na,b,c) -> GLetIn (dummy_loc,na,unloc b,unloc c)
+  | GCases (_,sty,rtntypopt,tml,pl) ->
+      GCases (dummy_loc,sty,
         (Option.map unloc rtntypopt),
 	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
-  | RLetTuple (_,nal,(na,po),b,c) ->
-      RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
-  | RIf (_,c,(na,po),b1,b2) ->
-      RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
-  | RRec (_,fk,idl,bl,tyl,bv) ->
-      RRec (dummy_loc,fk,idl,
+  | GLetTuple (_,nal,(na,po),b,c) ->
+      GLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
+  | GIf (_,c,(na,po),b1,b2) ->
+      GIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
+  | GRec (_,fk,idl,bl,tyl,bv) ->
+      GRec (dummy_loc,fk,idl,
             Array.map (List.map
               (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
-  | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t))
-  | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce)
-  | RSort (_,x) -> RSort (dummy_loc,x)
-  | RHole (_,x)  -> RHole (dummy_loc,x)
-  | RRef (_,x) -> RRef (dummy_loc,x)
-  | REvar (_,x,l) -> REvar (dummy_loc,x,l)
-  | RPatVar (_,x) -> RPatVar (dummy_loc,x)
-  | RDynamic (_,x) -> RDynamic (dummy_loc,x)
+  | GCast (_,c, CastConv (k,t)) -> GCast (dummy_loc,unloc c, CastConv (k,unloc t))
+  | GCast (_,c, CastCoerce) -> GCast (dummy_loc,unloc c, CastCoerce)
+  | GSort (_,x) -> GSort (dummy_loc,x)
+  | GHole (_,x)  -> GHole (dummy_loc,x)
+  | GRef (_,x) -> GRef (dummy_loc,x)
+  | GEvar (_,x,l) -> GEvar (dummy_loc,x,l)
+  | GPatVar (_,x) -> GPatVar (dummy_loc,x)
+  | GDynamic (_,x) -> GDynamic (dummy_loc,x)
 
 let anonymize_if_reserved na t = match na with
   | Name id as na ->
       (try
 	if not !Flags.raw_print &
-	   aconstr_of_rawconstr [] [] t = find_reserved_type id
-	then RHole (dummy_loc,Evd.BinderType na)
+	   aconstr_of_glob_constr [] [] t = find_reserved_type id
+	then GHole (dummy_loc,Evd.BinderType na)
 	else t
       with Not_found -> t)
   | Anonymous -> t