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

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 15bc06e02..2217074fe 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -248,48 +248,48 @@ let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
 let rec pat_of_raw metas vars = function
-  | RVar (_,id) ->
+  | GVar (_,id) ->
       (try PRel (list_index (Name id) vars)
        with Not_found -> PVar id)
-  | RPatVar (_,(false,n)) ->
+  | GPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
-  | RRef (_,gr) ->
+  | GRef (_,gr) ->
       PRef (canonical_gr gr)
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
-  | RApp (_, RPatVar (_,(true,n)), cl) ->
+  | GApp (_, GPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | RApp (_,c,cl) ->
+  | GApp (_,c,cl) ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-  | RLambda (_,na,bk,c1,c2) ->
+  | GLambda (_,na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RProd (_,na,bk,c1,c2) ->
+  | GProd (_,na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RLetIn (_,na,c1,c2) ->
+  | GLetIn (_,na,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RSort (_,s) ->
+  | GSort (_,s) ->
       PSort s
-  | RHole _ ->
+  | GHole _ ->
       PMeta None
-  | RCast (_,c,_) ->
+  | GCast (_,c,_) ->
       Flags.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
-  | RIf (_,c,(_,None),b1,b2) ->
+  | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
-  | RLetTuple (loc,nal,(_,None),b,c) ->
-      let mkRLambda c na = RLambda (loc,na,Explicit,RHole (loc,Evd.InternalHole),c) in
+  | GLetTuple (loc,nal,(_,None),b,c) ->
+      let mkRLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in
       let c = List.fold_left mkRLambda c nal in
       PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
              [|pat_of_raw metas vars c|])
-  | RCases (loc,sty,p,[c,(na,indnames)],brs) ->
+  | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
       let pred,ind_nargs, ind = match p,indnames with
 	| Some p, Some (_,ind,n,nal) ->
 	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
@@ -307,34 +307,34 @@ let rec pat_of_raw metas vars = function
              pat_of_raw metas vars c, brs)
 
   | r ->
-      let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.")
+      let loc = loc_of_glob_constr r in
+      user_err_loc (loc,"pattern_of_glob_constr", Pp.str"Non supported pattern.")
 
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
     (function
         (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
       | (loc,_,_,_) ->
-          user_err_loc (loc,"pattern_of_rawconstr",
+          user_err_loc (loc,"pattern_of_glob_constr",
                         Pp.str "Non supported pattern.")) brs in
   match bri with
     | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
 	if ind <> None & ind <> Some indsp then
-          user_err_loc (loc,"pattern_of_rawconstr",
+          user_err_loc (loc,"pattern_of_glob_constr",
             Pp.str "All constructors must be in the same inductive type.");
         let lna =
           List.map
             (function PatVar(_,na) -> na
               | PatCstr(loc,_,_,_) ->
-                  user_err_loc (loc,"pattern_of_rawconstr",
+                  user_err_loc (loc,"pattern_of_glob_constr",
                                 Pp.str "Non supported pattern.")) lv in
         let vars' = List.rev lna @ vars in
 	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
-    | _ -> user_err_loc (loc,"pattern_of_rawconstr",
+    | _ -> user_err_loc (loc,"pattern_of_glob_constr",
                          str "No unique branch for " ++ int (i+1) ++
                          str"-th constructor.")
 
-let pattern_of_rawconstr c =
+let pattern_of_glob_constr c =
   let metas = ref [] in
   let p = pat_of_raw metas [] c in	
   (!metas,p)