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

8 files changed, 16 insertions, 16 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e1d41b960..43c7e6e5a 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     try Pretyping.Default.understand_ltac true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
-      let loc = Rawterm.loc_of_rawconstr rawc in
+      let loc = Rawterm.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 7ce8a54c4..b800d0d66 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -17,7 +17,7 @@ open Rawterm
 (** Refinement of existential variables. *)
 
 val w_refine : evar * evar_info ->
-  rawconstr_ltac_closure -> evar_map -> evar_map
+  glob_constr_ltac_closure -> evar_map -> evar_map
 
 val instantiate_pf_com :
   Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 9f0d48bb1..a48bc2945 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -175,7 +175,7 @@ module Refinable = struct
       asks whether the term should have the same type as the conclusion.
       [resolve_classes] is a flag on pretyping functions which, if set to true,
       calls the typeclass resolver.
-      The principal argument is a [rawconstr] which is then pretyped in the
+      The principal argument is a [glob_constr] which is then pretyped in the
       context of a term, the remaining evars are registered to the handle.
       It is the main component of the toplevel refine tactic.*)
   (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
diff --git a/proofs/goal.mli b/proofs/goal.mli
index b291e1a77..3d9fcc5a2 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -69,11 +69,11 @@ module Refinable : sig
       The [check_type] argument asks whether the term should have the same
       type as the conclusion. [resolve_classes] is a flag on pretyping functions
       which, if set to true, calls the typeclass resolver.
-      The principal argument is a [rawconstr] which is then pretyped in the
+      The principal argument is a [glob_constr] which is then pretyped in the
       context of a term, the remaining evars are registered to the handle.
       It is the main component of the toplevel refine tactic.*)
   val constr_of_raw : 
-    handle -> bool -> bool -> Rawterm.rawconstr -> Term.constr sensitive
+    handle -> bool -> bool -> Rawterm.glob_constr -> Term.constr sensitive
 
 end
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index ff28ba877..ebb6db213 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -94,7 +94,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
   | LtacVarCall of identifier * glob_tactic_expr
-  | LtacConstrInterp of rawconstr *
+  | LtacConstrInterp of glob_constr *
       (extended_patvar_map * (identifier * identifier option) list)
 
 type ltac_trace = (int * loc * ltac_call_kind) list
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 886c0db42..cf73e0dca 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -124,7 +124,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
   | LtacVarCall of identifier * glob_tactic_expr
-  | LtacConstrInterp of rawconstr *
+  | LtacConstrInterp of glob_constr *
       (extended_patvar_map * (identifier * identifier option) list)
 
 type ltac_trace = (int * loc * ltac_call_kind) list
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 855d2cea7..b9e22ca05 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -262,8 +262,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
 
 (* Globalized tactics *)
 and glob_tactic_expr =
-    (rawconstr_and_expr,
-     rawconstr_and_expr * constr_pattern,
+    (glob_constr_and_expr,
+     glob_constr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -307,8 +307,8 @@ type raw_red_expr =
     (constr_expr, reference or_by_notation, constr_expr) red_expr_gen
 
 type glob_atomic_tactic_expr =
-    (rawconstr_and_expr,
-     rawconstr_and_expr * constr_pattern,
+    (glob_constr_and_expr,
+     glob_constr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -317,8 +317,8 @@ type glob_atomic_tactic_expr =
      glevel) gen_atomic_tactic_expr
 
 type glob_tactic_arg =
-    (rawconstr_and_expr,
-     rawconstr_and_expr * constr_pattern,
+    (glob_constr_and_expr,
+     glob_constr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -329,7 +329,7 @@ type glob_tactic_arg =
 type glob_generic_argument = glevel generic_argument
 
 type glob_red_expr =
-    (rawconstr_and_expr, evaluable_global_reference or_var, constr_pattern)
+    (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern)
     red_expr_gen
 
 type typed_generic_argument = tlevel generic_argument
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 42d81e863..d96f4c746 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -22,7 +22,7 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
 val set_match_pattern_printer :
   (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
 val set_match_rule_printer :
-  ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+  ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
     unit
 
 (** Debug information *)
@@ -39,7 +39,7 @@ val db_constr : debug_info -> env -> constr -> unit
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
+  debug_info -> int -> (Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :