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

diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
index 4657033869..9e872c236a 100644
--- a/plugins/funind/rawtermops.mli
+++ b/plugins/funind/rawtermops.mli
@@ -7,60 +7,60 @@ val idmap_is_empty : 'a Names.Idmap.t -> bool
 (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
 val get_pattern_id : cases_pattern -> Names.identifier list
 
-(* [pattern_to_term pat] returns a rawconstr corresponding to [pat].
+(* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
    [pat] must not contain occurences of anonymous pattern
 *)
-val pattern_to_term : cases_pattern -> rawconstr
+val pattern_to_term : cases_pattern -> glob_constr
 
 (*
-   Some basic functions to rebuild rawconstr
+   Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-val mkRRef : Libnames.global_reference -> rawconstr
-val mkRVar : Names.identifier -> rawconstr
-val mkRApp  : rawconstr*(rawconstr list) -> rawconstr
-val mkRLambda : Names.name * rawconstr * rawconstr -> rawconstr
-val mkRProd : Names.name * rawconstr * rawconstr -> rawconstr
-val mkRLetIn : Names.name * rawconstr * rawconstr -> rawconstr
-val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr
-val mkRSort : rawsort -> rawconstr
-val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
-val mkRCast : rawconstr* rawconstr -> rawconstr
+val mkRRef : Libnames.global_reference -> glob_constr
+val mkRVar : Names.identifier -> glob_constr
+val mkRApp  : glob_constr*(glob_constr list) -> glob_constr
+val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr
+val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr
+val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr
+val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
+val mkRSort : rawsort -> glob_constr
+val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
+val mkRCast : glob_constr* glob_constr -> glob_constr
 (*
-  Some basic functions to decompose rawconstrs
+  Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
-val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
-val raw_decompose_prod_or_letin :
-  rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr
-val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
-val raw_decompose_prod_or_letin_n : int -> rawconstr ->
-  (Names.name*rawconstr option*rawconstr option) list * rawconstr
-val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list  ->  rawconstr
-val raw_compose_prod_or_letin: rawconstr ->
-  (Names.name*rawconstr option*rawconstr option) list  ->  rawconstr
-val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
-
-
-(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-val  raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
-(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
-val  raw_make_neq : rawconstr -> rawconstr -> rawconstr
-(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
-val  raw_make_or : rawconstr -> rawconstr -> rawconstr
-
-(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
+val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr
+val glob_decompose_prod_or_letin :
+  glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr
+val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr
+val glob_decompose_prod_or_letin_n : int -> glob_constr ->
+  (Names.name*glob_constr option*glob_constr option) list * glob_constr
+val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list  ->  glob_constr
+val glob_compose_prod_or_letin: glob_constr ->
+  (Names.name*glob_constr option*glob_constr option) list  ->  glob_constr
+val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
+
+
+(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *)
+val  glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr
+(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
+val  glob_make_neq : glob_constr -> glob_constr -> glob_constr
+(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
+val  glob_make_or : glob_constr -> glob_constr -> glob_constr
+
+(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
    to [P1 \/ ( .... \/ Pn)]
 *)
-val  raw_make_or_list : rawconstr list -> rawconstr
+val  glob_make_or_list : glob_constr list -> glob_constr
 
 
 (* alpha_conversion functions *)
 
 
 
-(* Replace the var mapped in the rawconstr/context *)
-val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
+(* Replace the var mapped in the glob_constr/context *)
+val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
 
 
 
@@ -80,27 +80,27 @@ val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
 (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
    conventions and  does not share bound variables with avoid
 *)
-val alpha_rt : Names.identifier list -> rawconstr -> rawconstr
+val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
 val alpha_br : Names.identifier list ->
     Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.rawconstr ->
+    Rawterm.glob_constr ->
     Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.rawconstr
+    Rawterm.glob_constr
 
 
 (* Reduction function *)
 val replace_var_by_term  :
   Names.identifier ->
-  Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr
+  Rawterm.glob_constr -> Rawterm.glob_constr -> Rawterm.glob_constr
 
 
 
 (*
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
-val is_free_in : Names.identifier -> rawconstr -> bool
+val is_free_in : Names.identifier -> glob_constr -> bool
 
 
 val are_unifiable : cases_pattern -> cases_pattern -> bool
@@ -115,12 +115,12 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 val   ids_of_pat : cases_pattern -> Names.Idset.t
 
 (* TODO: finish this function (Fix not treated) *)
-val ids_of_rawterm: rawconstr -> Names.Idset.t
+val ids_of_rawterm: glob_constr -> Names.Idset.t
 
 (*
    removing let_in construction in a rawterm
 *)
-val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
+val zeta_normalize : Rawterm.glob_constr -> Rawterm.glob_constr
 
 
-val expand_as : rawconstr -> rawconstr
+val expand_as : glob_constr -> glob_constr