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

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