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

5 files changed, 9 insertions, 9 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index b37a27faf4..93b05290fc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -319,7 +319,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun ((_,indname),_,ar,lc) -> {
     ind_name = indname;
-    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.RType None)) ar;
+    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.GType None)) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
 
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index b26c3b88d9..87aedc7bea 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -35,7 +35,7 @@ val declare_rewriting_schemes : inductive -> unit
 (** Mutual Minimality/Induction scheme *)
 
 val do_mutual_induction_scheme :
-  (identifier located * bool * inductive * rawsort) list -> unit
+  (identifier located * bool * inductive * glob_sort) list -> unit
 
 (** Main calls to interpret the Scheme command *)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 707e0dc4a9..ea11ca487b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -30,7 +30,7 @@ open Topconstr
 
 let interp_evars evdref env impls k typ =
   let typ' = intern_gen true ~impls !evdref env typ in
-  let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
+  let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
 
 let interp_fields_evars evars env nots l =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 1b8271c89b..9af2224610 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -134,7 +134,7 @@ type option_ref_value =
   | StringRefValue of string
   | QualidRefValue of reference
 
-type sort_expr = Glob_term.rawsort
+type sort_expr = Glob_term.glob_sort
 
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index a6ef736174..67f54b523e 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -91,10 +91,10 @@ let uri_of_repr_kn ref (mp,dir,l) =
 let url_paren f l = url_char '('; f l; url_char ')'
 let url_bracket f l = url_char '['; f l; url_char ']'
 
-let whelp_of_rawsort = function
-  | RProp Null -> "Prop"
-  | RProp Pos -> "Set"
-  | RType _ -> "Type"
+let whelp_of_glob_sort = function
+  | GProp Null -> "Prop"
+  | GProp Pos -> "Set"
+  | GType _ -> "Type"
 
 let uri_int n = Buffer.add_string b (string_of_int n)
 
@@ -144,7 +144,7 @@ let rec uri_of_constr c =
   | GVar (_,id) -> url_id id
   | GRef (_,ref) ->  uri_of_global ref
   | GHole _ | GEvar _ -> url_string "?"
-  | GSort (_,s) -> url_string (whelp_of_rawsort s)
+  | GSort (_,s) -> url_string (whelp_of_glob_sort s)
   | _ -> url_paren (fun () -> match c with
   | GApp (_,f,args) ->
       let inst,rest = merge (section_parameters f) args in