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

12 files changed, 51 insertions, 51 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6abcd0314f..8e0d28fbfb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -196,22 +196,22 @@ let feed_history arg = function
 
 (* This is for non exhaustive error message *)
 
-let rec rawpattern_of_partial_history args2 = function
+let rec glob_pattern_of_partial_history args2 = function
   | Continuation (n, args1, h) ->
       let args3 = make_anonymous_patvars (n - (List.length args2)) in
-      build_rawpattern (List.rev_append args1 (args2@args3)) h
+      build_glob_pattern (List.rev_append args1 (args2@args3)) h
   | Result pl -> pl
 
-and build_rawpattern args = function
+and build_glob_pattern args = function
   | Top -> args
   | MakeAlias (AliasLeaf, rh) ->
       assert (args = []);
-      rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
+      glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
   | MakeAlias (AliasConstructor pci, rh) ->
-      rawpattern_of_partial_history
+      glob_pattern_of_partial_history
 	[PatCstr (dummy_loc, pci, args, Anonymous)] rh
 
-let complete_history = rawpattern_of_partial_history []
+let complete_history = glob_pattern_of_partial_history []
 
 (* This is to build glued pattern-matching history and alias bodies *)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4ff4cd3334..106629d2b0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -357,8 +357,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
-  | Prop c -> RProp c
-  | Type u -> RType (Some u)
+  | Prop c -> GProp c
+  | Type u -> GType (Some u)
 
 type binder_kind = BProd | BLambda | BLetIn
 
@@ -424,7 +424,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  GRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+  GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -440,7 +440,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) =
   let v = array_map2
     (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t))
     bodies tys in
-  GRec(dl,RCoFix n,Array.of_list (List.rev lfi),
+  GRec(dl,GCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index fd16c0013b..ff98f747e4 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -34,7 +34,7 @@ val detype_case :
   identifier list -> inductive * case_style * int * int array * int ->
     'a option -> 'a -> 'a array -> glob_constr
 
-val detype_sort : sorts -> rawsort
+val detype_sort : sorts -> glob_sort
 
 val detype_rel_context : constr option -> identifier list -> names_context ->
   rel_context -> glob_decl list
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index deba9a257a..b973a24f74 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -30,7 +30,7 @@ let cases_pattern_loc = function
 
 type patvar = identifier
 
-type rawsort = RProp of Term.contents | RType of Univ.universe option
+type glob_sort = GProp of Term.contents | GType of Univ.universe option
 
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
@@ -64,18 +64,18 @@ type glob_constr =
   | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
   | GRec of loc * fix_kind * identifier array * glob_decl list array *
       glob_constr array * glob_constr array
-  | GSort of loc * rawsort
+  | GSort of loc * glob_sort
   | GHole of (loc * hole_kind)
   | GCast of loc * glob_constr * glob_constr cast_type
   | GDynamic of loc * Dyn.t
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
 
-and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option
+and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option
 
 and fix_kind =
-  | RFix of ((int option * fix_recursion_order) array * int)
-  | RCoFix of int
+  | GFix of ((int option * fix_recursion_order) array * int)
+  | GCoFix of int
 
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
@@ -366,7 +366,7 @@ let glob_constr_of_closed_cases_pattern = function
 (**********************************************************************)
 (* Reduction expressions                                              *)
 
-type 'a raw_red_flag = {
+type 'a glob_red_flag = {
   rBeta : bool;
   rIota : bool;
   rZeta : bool;
@@ -392,8 +392,8 @@ type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
   | Simpl of 'c with_occurrences option
-  | Cbv of 'b raw_red_flag
-  | Lazy of 'b raw_red_flag
+  | Cbv of 'b glob_red_flag
+  | Lazy of 'b glob_red_flag
   | Unfold of 'b with_occurrences list
   | Fold of 'a list
   | Pattern of 'a with_occurrences list
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index 95305d58c2..4e11221d8b 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -31,7 +31,7 @@ val cases_pattern_loc : cases_pattern -> loc
 
 type patvar = identifier
 
-type rawsort = RProp of Term.contents | RType of Univ.universe option
+type glob_sort = GProp of Term.contents | GType of Univ.universe option
 
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
@@ -65,18 +65,18 @@ type glob_constr =
   | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
   | GRec of loc * fix_kind * identifier array * glob_decl list array *
       glob_constr array * glob_constr array
-  | GSort of loc * rawsort
+  | GSort of loc * glob_sort
   | GHole of (loc * Evd.hole_kind)
   | GCast of loc * glob_constr * glob_constr cast_type
   | GDynamic of loc * Dyn.t
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
 
-and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option
+and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option
 
 and fix_kind =
-  | RFix of ((int option * fix_recursion_order) array * int)
-  | RCoFix of int
+  | GFix of ((int option * fix_recursion_order) array * int)
+  | GCoFix of int
 
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
@@ -120,7 +120,7 @@ val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
 
 (** {6 Reduction expressions} *)
 
-type 'a raw_red_flag = {
+type 'a glob_red_flag = {
   rBeta : bool;
   rIota : bool;
   rZeta : bool;
@@ -128,7 +128,7 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
-val all_flags : 'a raw_red_flag
+val all_flags : 'a glob_red_flag
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 
@@ -145,8 +145,8 @@ type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
   | Simpl of 'c with_occurrences option
-  | Cbv of 'b raw_red_flag
-  | Lazy of 'b raw_red_flag
+  | Cbv of 'b glob_red_flag
+  | Lazy of 'b glob_red_flag
   | Unfold of 'b with_occurrences list
   | Fold of 'a list
   | Pattern of 'a with_occurrences list
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index fc56f31d3f..1facb7c7ab 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -173,9 +173,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
       | PRel n1, Rel n2 when n1 = n2 -> subst
 
-      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst
+      | PSort (GProp c1), Sort (Prop c2) when c1 = c2 -> subst
 
-      | PSort (RType _), Sort (Type _) -> subst
+      | PSort (GType _), Sort (Type _) -> subst
 
       | PApp (p, [||]), _ -> sorec stk subst p t
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 19c5d156a1..50dd413c68 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -36,7 +36,7 @@ type constr_pattern =
   | PLambda of name * constr_pattern * constr_pattern
   | PProd of name * constr_pattern * constr_pattern
   | PLetIn of name * constr_pattern * constr_pattern
-  | PSort of rawsort
+  | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of (case_style * int array * inductive option * (int * int) option)
@@ -92,8 +92,8 @@ let pattern_of_constr sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
-    | Sort (Prop c) -> PSort (RProp c)
-    | Sort (Type _) -> PSort (RType None)
+    | Sort (Prop c) -> PSort (GProp c)
+    | Sort (Type _) -> PSort (GType None)
     | Cast (c,_,_)      -> pattern_of_constr c
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
@@ -300,7 +300,7 @@ let rec pat_of_raw metas vars = function
 	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	  | _ -> None in
       let cbrs =
-	Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
+	Array.init (List.length brs) (pat_of_glob_branch loc metas vars ind brs)
       in
       let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
       PCase ((sty,cstr_nargs,ind,ind_nargs), pred,
@@ -310,7 +310,7 @@ let rec pat_of_raw metas vars = function
       let loc = loc_of_glob_constr r in
       user_err_loc (loc,"pattern_of_glob_constr", Pp.str"Non supported pattern.")
 
-and pat_of_raw_branch loc metas vars ind brs i =
+and pat_of_glob_branch loc metas vars ind brs i =
   let bri = List.filter
     (function
         (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index b25637de9e..23de675989 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -70,7 +70,7 @@ type constr_pattern =
   | PLambda of name * constr_pattern * constr_pattern
   | PProd of name * constr_pattern * constr_pattern
   | PLetIn of name * constr_pattern * constr_pattern
-  | PSort of rawsort
+  | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of (case_style * int array * inductive option * (int * int) option)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index b331574140..c0fa620485 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -183,7 +183,7 @@ let error_unexpected_type_loc loc env sigma actty expty =
 let error_not_product_loc loc env sigma c =
   raise_pretype_error (loc, env, sigma, NotProduct c)
 
-(*s Error in conversion from AST to rawterms *)
+(*s Error in conversion from AST to glob_constr *)
 
 let error_var_not_found_loc loc s =
   raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 11722bee2d..b558020440 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -123,6 +123,6 @@ val error_unexpected_type_loc :
 val error_not_product_loc :
   loc -> env -> Evd.evar_map -> constr -> 'b
 
-(** {6 Error in conversion from AST to rawterms } *)
+(** {6 Error in conversion from AST to glob_constr } *)
 
 val error_var_not_found_loc : loc -> identifier -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index baa783d0c6..a2fb8ea12d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -93,13 +93,13 @@ let ((constr_in : constr -> Dyn.t),
 (** Miscellaneous interpretation functions *)
 
 let interp_sort = function
-  | RProp c -> Prop c
-  | RType _ -> new_Type_sort ()
+  | GProp c -> Prop c
+  | GType _ -> new_Type_sort ()
 
 let interp_elimination_sort = function
-  | RProp Null -> InProp
-  | RProp Pos  -> InSet
-  | RType _ -> InType
+  | GProp Null -> InProp
+  | GProp Pos  -> InSet
+  | GType _ -> InType
 
 module type S =
 sig
@@ -122,7 +122,7 @@ sig
   (* More general entry point with evars from ltac *)
 
   (* Generic call to the interpreter from glob_constr to constr, failing
-     unresolved holes in the rawterm cannot be instantiated.
+     unresolved holes in the glob_constr cannot be instantiated.
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
@@ -293,8 +293,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       make_judge c (Retyping.get_type_of env Evd.empty c)
 
   let pretype_sort = function
-    | RProp c -> judge_of_prop_contents c
-    | RType _ -> judge_of_new_Type ()
+    | GProp c -> judge_of_prop_contents c
+    | GType _ -> judge_of_new_Type ()
 
   exception Found of fixpoint
 
@@ -381,7 +381,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let ftys = Array.map (nf_evar !evdref) ftys in
 	let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
  	let fixj = match fixkind with
-	  | RFix (vn,i) ->
+	  | GFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
 	      (* If recursive argument was not given by user, we try all args.
 	         An earlier approach was to look only for inductive arguments,
@@ -397,7 +397,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      let fixdecls = (names,ftys,fdefs) in
 	      let indexes = search_guard loc env possible_indexes fixdecls in
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
-	  | RCoFix i ->
+	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 70e1a22fb6..e1f79f36c5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -53,7 +53,7 @@ sig
   (** More general entry point with evars from ltac *)
 
   (** Generic call to the interpreter from glob_constr to constr, failing
-     unresolved holes in the rawterm cannot be instantiated.
+     unresolved holes in the glob_constr cannot be instantiated.
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
@@ -114,6 +114,6 @@ module Default : S
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr
 
-val interp_sort : rawsort -> sorts
-val interp_elimination_sort : rawsort -> sorts_family
+val interp_sort : glob_sort -> sorts
+val interp_elimination_sort : glob_sort -> sorts_family