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

3 files changed, 21 insertions, 21 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index d14b8cccc..04e0b352c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -855,7 +855,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	   let filter =
 	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
 	   let unboundvars = list_map_filter filter unboundvars in
-	   quote (pr_rawconstr_env (Global.env()) c) ++
+	   quote (pr_glob_constr_env (Global.env()) c) ++
 	     (if unboundvars <> [] or vars <> [] then
 		strbrk " (with " ++
 		  prlist_with_sep pr_comma
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 78235f458..1265fe02b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -798,7 +798,7 @@ let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let t = Constrintern.interp_type Evd.empty (Global.env()) c in
     let t = Detyping.detype false [] [] t in
-    let t = aconstr_of_rawconstr [] [] t in
+    let t = aconstr_of_glob_constr [] [] t in
     List.iter (fun id -> Reserve.declare_reserved_type id t) idl)
   in List.iter sb_decl bl
 
@@ -1121,11 +1121,11 @@ let vernac_print = function
   | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
   | PrintHintDb -> Auto.print_searchtable ()
   | PrintScopes ->
-      pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
+      pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
   | PrintScope s ->
-      pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s)
+      pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintVisibility s ->
-      pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
+      pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintAbout qid -> msg (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
@@ -1187,7 +1187,7 @@ let vernac_locate = function
   | LocateTerm (Genarg.ByNotation (_,ntn,sc)) ->
       ppnl
         (Notation.locate_notation
-          (Constrextern.without_symbols pr_lrawconstr) ntn sc)
+          (Constrextern.without_symbols pr_lglob_constr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> print_located_module qid
   | LocateTactic qid -> print_located_tactic qid
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 906629997..dd947fcda 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -127,9 +127,9 @@ let uri_params f = function
 let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
 
 let section_parameters = function
-  | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+  | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
       get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
-  | RRef (_,(ConstRef cst as ref)) ->
+  | GRef (_,(ConstRef cst as ref)) ->
       get_discharged_hyp_names (path_of_global ref)
   | _ -> []
 
@@ -141,33 +141,33 @@ let merge vl al =
 
 let rec uri_of_constr c =
   match c with
-  | RVar (_,id) -> url_id id
-  | RRef (_,ref) ->  uri_of_global ref
-  | RHole _ | REvar _ -> url_string "?"
-  | RSort (_,s) -> url_string (whelp_of_rawsort s)
+  | GVar (_,id) -> url_id id
+  | GRef (_,ref) ->  uri_of_global ref
+  | GHole _ | GEvar _ -> url_string "?"
+  | GSort (_,s) -> url_string (whelp_of_rawsort s)
   | _ -> url_paren (fun () -> match c with
-  | RApp (_,f,args) ->
+  | GApp (_,f,args) ->
       let inst,rest = merge (section_parameters f) args in
       uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
       url_list_with_sep " " uri_of_constr rest
-  | RLambda (_,na,k,ty,c) ->
+  | GLambda (_,na,k,ty,c) ->
       url_string "\\lambda "; url_of_name na; url_string ":";
       uri_of_constr ty; url_string "."; uri_of_constr c
-  | RProd (_,Anonymous,k,ty,c) ->
+  | GProd (_,Anonymous,k,ty,c) ->
       uri_of_constr ty; url_string "\\to "; uri_of_constr c
-  | RProd (_,Name id,k,ty,c) ->
+  | GProd (_,Name id,k,ty,c) ->
       url_string "\\forall "; url_id id; url_string ":";
       uri_of_constr ty; url_string "."; uri_of_constr c
-  | RLetIn (_,na,b,c) ->
+  | GLetIn (_,na,b,c) ->
       url_string "let "; url_of_name na; url_string "\\def ";
       uri_of_constr b; url_string " in "; uri_of_constr c
-  | RCast (_,c, CastConv (_,t)) ->
+  | GCast (_,c, CastConv (_,t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
-  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+  | GRec _ | GIf _ | GLetTuple _ | GCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint."
-  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
+  | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"
-  | RPatVar _ | RDynamic _ ->
+  | GPatVar _ | GDynamic _ ->
       anomaly "Found constructors not supported in constr") ()
 
 let make_string f x = Buffer.reset b; f x; Buffer.contents b