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

5 files changed, 5 insertions, 5 deletions

diff --git a/dev/base_include b/dev/base_include
index 23cc38fb47..19c0f4b4e1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -171,7 +171,7 @@ let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
 let parse_tac    = Pcoq.parse_string Pcoq.Tactic.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
-(* build a term of type rawconstr without type-checking or resolution of 
+(* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
 
 let e s =
diff --git a/dev/db b/dev/db
index 9eed32e040..e7225e8f24 100644
--- a/dev/db
+++ b/dev/db
@@ -17,7 +17,7 @@ install_printer Top_printers.ppclindex
 install_printer Top_printers.ppbigint
 
 install_printer Top_printers.pppattern
-install_printer Top_printers.pprawconstr
+install_printer Top_printers.ppglob_constr
 
 install_printer Top_printers.ppconstr
 install_printer Top_printers.ppuni
diff --git a/dev/include b/dev/include
index 251a969b9c..b72e68ac07 100644
--- a/dev/include
+++ b/dev/include
@@ -14,7 +14,7 @@
 #install_printer  (* pp_stdcmds *) pppp;;
 
 #install_printer  (* pattern *) pppattern;;
-#install_printer  (* rawconstr *) pprawconstr;;
+#install_printer  (* glob_constr *) ppglob_constr;;
 
 #install_printer  (* constr *) ppconstr;;
 #install_printer  (* constr_substituted *) ppsconstr;; 
diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro
index 20c3de5efc..33d20fc818 100644
--- a/dev/ocamldoc/docintro
+++ b/dev/ocamldoc/docintro
@@ -30,7 +30,7 @@ describes the Coq library, which is made of two parts:
 
 describes the translation from Coq context-dependent
 front abstract syntax of terms {v constr_expr v} to and from the
-context-free, untyped, globalized form of constructions {v rawconstr v}.}
+context-free, untyped, globalized form of constructions {v glob_constr v}.}
 {- Parsers and printers : parsing
 
 describes the implementation of the Coq parsers and printers.}
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1f05e90bde..89a6eb5e32 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -56,7 +56,7 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
 let ppsconstr x = ppconstr (Declarations.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
-let pprawconstr = (fun x -> pp(pr_lrawconstr x))
+let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
 let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))