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

7 files changed, 54 insertions, 54 deletions

diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index a35eb419d1..de3fbb683e 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -135,37 +135,37 @@ let compute_branches_lengths ind =
 let compute_inductive_nargs ind =
   Inductiveops.inductive_nargs (Global.env()) ind
 
-(* Interpreting constr as a rawconstr *)
+(* Interpreting constr as a glob_constr *)
 
 let rec interp_xml_constr = function
   | XmlTag (loc,"REL",al,[]) ->
-      RVar (loc, get_xml_ident al)
+      GVar (loc, get_xml_ident al)
   | XmlTag (loc,"VAR",al,[]) ->
       error "XML parser: unable to interp free variables"
   | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
       let body,decls = list_sep_last xl in
       let ctx = List.map interp_xml_decl decls in
-      List.fold_right (fun (na,t) b -> RLambda (loc, na, Explicit, t, b))
+      List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
 	ctx (interp_xml_target body)
   | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
       let body,decls = list_sep_last xl in
       let ctx = List.map interp_xml_decl decls in
-      List.fold_right (fun (na,t) b -> RProd (loc, na, Explicit, t, b))
+      List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
 	ctx (interp_xml_target body)
   | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
       let body,defs = list_sep_last xl in
       let ctx = List.map interp_xml_def defs in
-      List.fold_right (fun (na,t) b -> RLetIn (loc, na, t, b))
+      List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
         ctx (interp_xml_target body)
   | XmlTag (loc,"APPLY",_,x::xl) ->
-      RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
+      GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
   | XmlTag (loc,"instantiate",_,
       (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
-      RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
+      GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
   | XmlTag (loc,"META",al,xl) ->
-      REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
+      GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
   | XmlTag (loc,"CONST",al,[]) ->
-      RRef (loc, ConstRef (get_xml_constant al))
+      GRef (loc, ConstRef (get_xml_constant al))
   | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
       let ind = get_xml_inductive al in
       let p = interp_xml_patternsType x in
@@ -175,23 +175,23 @@ let rec interp_xml_constr = function
       let mat = simple_cases_matrix_of_branches ind brns brs in
       let nparams,n = compute_inductive_nargs ind in
       let nal,rtn = return_type_of_predicate ind nparams n p in
-      RCases (loc,RegularStyle,rtn,[tm,nal],mat)
+      GCases (loc,RegularStyle,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
-      RRef (loc, IndRef (get_xml_inductive al))
+      GRef (loc, IndRef (get_xml_inductive al))
   | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
-      RRef (loc, ConstructRef (get_xml_constructor al))
+      GRef (loc, ConstructRef (get_xml_constructor al))
   | XmlTag (loc,"FIX",al,xl) ->
       let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
       let ln,lc,lt = list_split3 lnct in
       let lctx = List.map (fun _ -> []) ln in
-      RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
+      GRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"COFIX",al,xl) ->
       let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
-      RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
+      GRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"CAST",al,[x1;x2]) ->
-      RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
+      GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
   | XmlTag (loc,"SORT",al,[]) ->
-      RSort (loc, get_xml_sort al)
+      GSort (loc, get_xml_sort al)
   | XmlTag (loc,s,_,_) ->
       user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6f0896cc89..0dea0d2acb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -39,8 +39,8 @@ type 'a raw_extra_genarg_printer =
     'a -> std_ppcmds
 
 type 'a glob_extra_genarg_printer =
-    (rawconstr_and_expr -> std_ppcmds) ->
-    (rawconstr_and_expr -> std_ppcmds) ->
+    (glob_constr_and_expr -> std_ppcmds) ->
+    (glob_constr_and_expr -> std_ppcmds) ->
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     'a -> std_ppcmds
 
@@ -958,7 +958,7 @@ let strip_prod_binders_rawterm n (ty,_) =
   let rec strip_ty acc n ty =
     if n=0 then (List.rev acc, (ty,None)) else
       match ty with
-          Rawterm.RProd(loc,na,Explicit,a,b) ->
+          Rawterm.GProd(loc,na,Explicit,a,b) ->
             strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
@@ -995,13 +995,13 @@ and pr_raw_tactic_level env n (t:raw_tactic_expr) =
 let pr_and_constr_expr pr (c,_) = pr c
 
 let pr_pat_and_constr_expr b (c,_) =
-  pr_and_constr_expr ((if b then pr_lrawconstr_env else pr_rawconstr_env)
+  pr_and_constr_expr ((if b then pr_lglob_constr_env else pr_glob_constr_env)
     (Global.env())) c
 
 let rec glob_printers =
     (pr_glob_tactic_level,
-     (fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
-     (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
+     (fun env -> pr_and_constr_expr (pr_glob_constr_env env)),
+     (fun env -> pr_and_constr_expr (pr_lglob_constr_env env)),
      pr_pat_and_constr_expr,
      (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
      (fun env -> pr_or_var (pr_inductive env)),
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 71fe03e70e..21de95ba04 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -30,8 +30,8 @@ type 'a raw_extra_genarg_printer =
     'a -> std_ppcmds
 
 type 'a glob_extra_genarg_printer =
-    (rawconstr_and_expr -> std_ppcmds) ->
-    (rawconstr_and_expr -> std_ppcmds) ->
+    (glob_constr_and_expr -> std_ppcmds) ->
+    (glob_constr_and_expr -> std_ppcmds) ->
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     'a -> std_ppcmds
 
@@ -70,9 +70,9 @@ val pr_raw_extend:
     string -> raw_generic_argument list -> std_ppcmds
 
 val pr_glob_extend:
-  (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) ->
+  (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
   (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-  (rawconstr_pattern_and_expr -> std_ppcmds) -> int ->
+  (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
     string -> glob_generic_argument list -> std_ppcmds
 
 val pr_extend :
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4ea3b1591d..3b979f519b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -460,10 +460,10 @@ let gallina_print_syntactic_def kn =
   let sep = " := "
   and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
-  let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
+  let c = Topconstr.glob_constr_of_aconstr dummy_loc a in
   str "Notation " ++ pr_qualid qid ++
   prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
-  Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
+  Constrextern.without_symbols pr_lglob_constr c ++ fnl ()
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c575fde52b..a7fa08f502 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -86,15 +86,15 @@ let pr_ljudge_env env j =
 
 let pr_ljudge j = pr_ljudge_env (Global.env()) j
 
-let pr_lrawconstr_env env c =
-  pr_lconstr_expr (extern_rawconstr (Termops.vars_of_env env) c)
-let pr_rawconstr_env env c =
-  pr_constr_expr (extern_rawconstr (Termops.vars_of_env env) c)
+let pr_lglob_constr_env env c =
+  pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+let pr_glob_constr_env env c =
+  pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
 
-let pr_lrawconstr c =
-  pr_lconstr_expr (extern_rawconstr Idset.empty c)
-let pr_rawconstr c =
-  pr_constr_expr (extern_rawconstr Idset.empty c)
+let pr_lglob_constr c =
+  pr_lconstr_expr (extern_glob_constr Idset.empty c)
+let pr_glob_constr c =
+  pr_constr_expr (extern_glob_constr Idset.empty c)
 
 let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
@@ -128,7 +128,7 @@ let pr_evaluable_reference ref =
   pr_global (Tacred.global_of_evaluable_reference ref)
 
 (*let pr_rawterm t =
-  pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*)
+  pr_lconstr (Constrextern.extern_glob_constr Idset.empty t)*)
 
 (*open Pattern
 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 11bebbd499..2da3678161 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -54,11 +54,11 @@ val pr_type                : types -> std_ppcmds
 val pr_ljudge_env          : env -> unsafe_judgment -> std_ppcmds * std_ppcmds
 val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
 
-val pr_lrawconstr_env      : env -> rawconstr -> std_ppcmds
-val pr_lrawconstr          : rawconstr -> std_ppcmds
+val pr_lglob_constr_env      : env -> glob_constr -> std_ppcmds
+val pr_lglob_constr          : glob_constr -> std_ppcmds
 
-val pr_rawconstr_env       : env -> rawconstr -> std_ppcmds
-val pr_rawconstr           : rawconstr -> std_ppcmds
+val pr_glob_constr_env       : env -> glob_constr -> std_ppcmds
+val pr_glob_constr           : glob_constr -> std_ppcmds
 
 val pr_lconstr_pattern_env : env -> constr_pattern -> std_ppcmds
 val pr_lconstr_pattern     : constr_pattern -> std_ppcmds
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 348905cad6..7b0576a321 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -23,14 +23,14 @@ let dloc = <:expr< Util.dummy_loc >>
 
 let apply_ref f l =
   <:expr<
-    Rawterm.RApp ($dloc$, Rawterm.RRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$)
+    Rawterm.GApp ($dloc$, Rawterm.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$)
   >>
 
 EXTEND
   GLOBAL: expr;
   expr:
     [ [ "PATTERN"; "["; c = constr; "]" ->
-      <:expr< snd (Pattern.pattern_of_rawconstr $c$) >> ] ]
+      <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ]
   ;
   sort:
     [ [ "Set"  -> RProp Pos
@@ -49,19 +49,19 @@ EXTEND
   constr:
     [ "200" RIGHTA
       [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr ->
-        <:expr< Rawterm.RProd ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >>
+        <:expr< Rawterm.GProd ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >>
       | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr ->
-        <:expr< Rawterm.RLambda ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >>
+        <:expr< Rawterm.GLambda ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >>
       | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr ->
         <:expr< Rawterm.RLetin ($dloc$,Name $id$,$c1$,$c2$) >>
       (* fix todo *)
       ]
     | "100" RIGHTA
       [ c1 = constr; ":"; c2 = SELF ->
-        <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
+        <:expr< Rawterm.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
     | "90" RIGHTA
       [ c1 = constr; "->"; c2 = SELF ->
-        <:expr< Rawterm.RProd ($dloc$,Anonymous,Rawterm.Explicit,$c1$,$c2$) >> ]
+        <:expr< Rawterm.GProd ($dloc$,Anonymous,Rawterm.Explicit,$c1$,$c2$) >> ]
     | "75" RIGHTA
       [ "~"; c = constr ->
         apply_ref <:expr< coq_not_ref >> [c] ]
@@ -71,15 +71,15 @@ EXTEND
     | "10" LEFTA
       [ f = constr; args = LIST1 NEXT ->
         let args = mlexpr_of_list (fun x -> x) args in
-        <:expr< Rawterm.RApp ($dloc$,$f$,$args$) >> ]
+        <:expr< Rawterm.GApp ($dloc$,$f$,$args$) >> ]
     | "0"
-      [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
-      | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
-      | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >>
-      | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
+      [ s = sort -> <:expr< Rawterm.GSort ($dloc$,s) >>
+      | id = ident -> <:expr< Rawterm.GVar ($dloc$,$id$) >>
+      | "_" -> <:expr< Rawterm.GHole ($dloc$, QuestionMark (Define False)) >>
+      | "?"; id = ident -> <:expr< Rawterm.GPatVar($dloc$,(False,$id$)) >>
       | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
           apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
-      | "%"; e = string -> <:expr< Rawterm.RRef ($dloc$,Lazy.force $lid:e$) >>
+      | "%"; e = string -> <:expr< Rawterm.GRef ($dloc$,Lazy.force $lid:e$) >>
       | c = match_constr -> c
       | "("; c = constr LEVEL "200"; ")" -> c ] ]
   ;
@@ -87,7 +87,7 @@ EXTEND
     [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type;
         "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" ->
           let br = mlexpr_of_list (fun x -> x) br in
-     <:expr< Rawterm.RCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >>
+     <:expr< Rawterm.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >>
     ] ]
   ;
   match_type: