More {raw => glob} changes for consistency

perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat
tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\
W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s
/glob_terms?/glob_constr/g' **/*.ml*

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 32 insertions, 32 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index d8574409db..6a01ff1dcf 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -133,9 +133,9 @@ GEXTEND Gram
     [ [ c = lconstr -> c ] ]
   ;
   sort:
-    [ [ "Set"  -> RProp Pos
-      | "Prop" -> RProp Null
-      | "Type" -> RType None ] ]
+    [ [ "Set"  -> GProp Pos
+      | "Prop" -> GProp Null
+      | "Type" -> GType None ] ]
   ;
   lconstr:
     [ [ c = operconstr LEVEL "200" -> c ] ]
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 18bc1ff782..72634b08e7 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -95,9 +95,9 @@ let inductive_of_cdata a = match global_of_cdata a with
 let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
 
 let sort_of_cdata (loc,a) = match a with
-  | "Prop" -> RProp Null
-  | "Set" -> RProp Pos
-  | "Type" -> RType None
+  | "Prop" -> GProp Null
+  | "Set" -> GProp Pos
+  | "Type" -> GType None
   | _ -> user_err_loc (loc,"",str "sort expected.")
 
 let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
@@ -184,10 +184,10 @@ let rec interp_xml_constr = function
       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
-      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)
+      GRec (loc, GFix (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
-      GRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
+      GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"CAST",al,[x1;x2]) ->
       GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
   | XmlTag (loc,"SORT",al,[]) ->
@@ -229,15 +229,15 @@ and interp_xml_recursionOrder x =
   let (locs, s) = get_xml_attr "type" al in
     match s with
 	"Structural" ->
-	  (match l with [] -> RStructRec
+	  (match l with [] -> GStructRec
 	     | _ -> error_expect_no_argument loc)
       | "WellFounded" ->
 	  (match l with
-	       [c] -> RWfRec (interp_xml_type c)
+	       [c] -> GWfRec (interp_xml_type c)
 	     | _ -> error_expect_one_argument loc)
       | "Measure" ->
 	  (match l with
-	       [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+	       [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
 	     | _ -> error_expect_two_arguments loc)
       | _ ->
           user_err_loc (locs,"",str "Invalid recursion order.")
@@ -249,7 +249,7 @@ and interp_xml_FixFunction x =
 	interp_xml_recursionOrder x1),
        (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
   | (loc,al,[x1;x2]) ->
-      ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
+      ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
        (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
   | (loc,_,_) ->
       error_expect_one_argument loc
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 68d434a2b3..bba0e56022 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -187,7 +187,7 @@ module Constr :
     val operconstr : constr_expr Gram.entry
     val ident : identifier Gram.entry
     val global : reference Gram.entry
-    val sort : rawsort Gram.entry
+    val sort : glob_sort Gram.entry
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 9e9d21a3de..54dd550d8c 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -108,10 +108,10 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 
 let pr_universe = Univ.pr_uni
 
-let pr_rawsort = function
-  | RProp Term.Null -> str "Prop"
-  | RProp Term.Pos -> str "Set"
-  | RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
+let pr_glob_sort = function
+  | GProp Term.Null -> str "Prop"
+  | GProp Term.Pos -> str "Set"
+  | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
 
 let pr_id = pr_id
 let pr_name = pr_name
@@ -515,7 +515,7 @@ let pr pr sep inherited a =
   | CHole _ -> str "_", latom
   | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
-  | CSort (_,s) -> pr_rawsort s, latom
+  | CSort (_,s) -> pr_glob_sort s, latom
   | CCast (_,a,CastConv (k,b)) ->
       let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 49791d5957..f9ed3af02f 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -56,7 +56,7 @@ val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
   ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds
 
-val pr_rawsort : rawsort -> std_ppcmds
+val pr_glob_sort : glob_sort -> std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
 val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
@@ -84,7 +84,7 @@ val default_term_pr : term_pr
     for instance if we want to build a printer which prints "Prop" as "Omega"
     instead we can proceed as follows:
     let my_modular_constr_pr pr s p = function
-      | CSort (_,RProp Null) -> str "Omega"
+      | CSort (_,GProp Null) -> str "Omega"
       | t -> modular_constr_pr pr s p t
     Which has the same type. We can turn a modular printer into a printer by
     taking its fixpoint. *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 015dc9c081..9da14d8fa6 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -140,7 +140,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x)
   | VarArgType -> pr_located pr_id (out_gen rawwit_var x)
   | RefArgType -> prref (out_gen rawwit_ref x)
-  | SortArgType -> pr_rawsort (out_gen rawwit_sort x)
+  | SortArgType -> pr_glob_sort (out_gen rawwit_sort x)
   | ConstrArgType -> prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
       pr_may_eval prc prlc (pr_or_by_notation prref) prpat
@@ -183,7 +183,7 @@ let rec pr_glob_generic prc prlc prtac prpat x =
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x)
   | VarArgType -> pr_located pr_id (out_gen globwit_var x)
   | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
-  | SortArgType -> pr_rawsort (out_gen globwit_sort x)
+  | SortArgType -> pr_glob_sort (out_gen globwit_sort x)
   | ConstrArgType -> prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
       pr_may_eval prc prlc
@@ -954,7 +954,7 @@ and pr_tacarg = function
 
 in (pr_tac, pr_match_rule)
 
-let strip_prod_binders_rawterm n (ty,_) =
+let strip_prod_binders_glob_constr n (ty,_) =
   let rec strip_ty acc n ty =
     if n=0 then (List.rev acc, (ty,None)) else
       match ty with
@@ -1008,7 +1008,7 @@ let rec glob_printers =
      pr_ltac_or_var (pr_located pr_ltac_constant),
      pr_lident,
      pr_glob_extend,
-     strip_prod_binders_rawterm)
+     strip_prod_binders_glob_constr)
 
 and pr_glob_tactic_level env n (t:glob_tactic_expr) =
   fst (make_pr_tac glob_printers env) n t
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b5367048a5..8d74fd1f83 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -307,7 +307,7 @@ let pr_onescheme (idop,schem) =
     ) ++
     hov 0 ((if dep then str"Induction for" else str"Minimality for")
     ++ spc() ++ pr_smart_global ind) ++ spc() ++
-    hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
+    hov 0 (str"Sort" ++ spc() ++ pr_glob_sort s)
   | CaseScheme (dep,ind,s) ->
     (match idop with
       | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
@@ -315,7 +315,7 @@ let pr_onescheme (idop,schem) =
     ) ++
     hov 0 ((if dep then str"Elimination for" else str"Case for")
     ++ spc() ++ pr_smart_global ind) ++ spc() ++
-    hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
+    hov 0 (str"Sort" ++ spc() ++ pr_glob_sort s)
   | EqualityScheme ind ->
     (match idop with
       | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
@@ -673,7 +673,7 @@ let rec pr_vernac = function
 (* 	str"Class" ++ spc () ++ pr_lident id ++ *)
 (* (\* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *\) *)
 (* 	  pr_and_type_binders_arg par ++ *)
-(* 	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++ *)
+(* 	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_glob_sort (snd ar) | None -> mt()) ++ *)
 (* 	  spc () ++ str":=" ++ spc () ++ *)
 (* 	  prlist_with_sep (fun () -> str";" ++ spc())  *)
 (* 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index a7fa08f502..f1f5d4c9f3 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -109,7 +109,7 @@ let pr_lconstr_pattern t =
 let pr_constr_pattern t =
   pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
 
-let pr_sort s = pr_rawsort (extern_sort s)
+let pr_sort s = pr_glob_sort (extern_sort s)
 
 let _ = Termops.set_print_constr pr_lconstr_env
 
@@ -127,7 +127,7 @@ let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
 let pr_evaluable_reference ref =
   pr_global (Tacred.global_of_evaluable_reference ref)
 
-(*let pr_rawterm t =
+(*let pr_glob_constr t =
   pr_lconstr (Constrextern.extern_glob_constr Idset.empty t)*)
 
 (*open Pattern
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index c8451afb16..605432692b 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -33,9 +33,9 @@ EXTEND
       <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ]
   ;
   sort:
-    [ [ "Set"  -> RProp Pos
-      | "Prop" -> RProp Null
-      | "Type" -> RType None ] ]
+    [ [ "Set"  -> GProp Pos
+      | "Prop" -> GProp Null
+      | "Type" -> GType None ] ]
   ;
   ident:
     [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ]