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

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9215f9b517..fa0e189153 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -487,7 +487,7 @@ let rec flatten_application = function
   | a -> a
 
 (**********************************************************************)
-(* mapping rawterms to numerals (in presence of coercions, choose the *)
+(* mapping glob_constr to numerals (in presence of coercions, choose the *)
 (* one with no delimiter if possible)                                 *)
 
 let extern_possible_prim_token scopes r =
@@ -507,12 +507,12 @@ let extern_optimal_prim_token scopes r r' =
   | _ -> raise No_match
 
 (**********************************************************************)
-(* mapping rawterms to constr_expr                                    *)
+(* mapping glob_constr to constr_expr                                    *)
 
-let extern_rawsort = function
-  | RProp _ as s -> s
-  | RType (Some _) as s when !print_universes -> s
-  | RType _ -> RType None
+let extern_glob_sort = function
+  | GProp _ as s -> s
+  | GType (Some _) as s when !print_universes -> s
+  | GType _ -> GType None
 
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
@@ -646,7 +646,7 @@ let rec extern inctx scopes vars r =
   | GRec (loc,fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Idset.add idv vars in
       (match fk with
-	 | RFix (nv,n) ->
+	 | GFix (nv,n) ->
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
@@ -663,7 +663,7 @@ let rec extern inctx scopes vars r =
                   extern false scopes vars1 def)) idv
 	     in
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
-	 | RCoFix n ->
+	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
                  let (ids,bl) = extern_local_binder scopes vars blv.(i) in
@@ -674,7 +674,7 @@ let rec extern inctx scopes vars r =
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
-  | GSort (loc,s) -> CSort (loc,extern_rawsort s)
+  | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
 
   | GHole (loc,e) -> CHole (loc, Some e)
 
@@ -809,9 +809,9 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	  No_match -> extern_symbol allscopes vars t rules
 
 and extern_recursion_order scopes vars = function
-    RStructRec -> CStructRec
-  | RWfRec c -> CWfRec (extern true scopes vars c)
-  | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
+    GStructRec -> CStructRec
+  | GWfRec c -> CWfRec (extern true scopes vars c)
+  | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
 				     Option.map (extern true scopes vars) r)
 
 
@@ -843,15 +843,15 @@ let extern_type at_top env t =
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   extern_glob_type (vars_of_env env) r
 
-let extern_sort s = extern_rawsort (detype_sort s)
+let extern_sort s = extern_glob_sort (detype_sort s)
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
-let rec raw_of_pat env = function
+let rec glob_of_pat env = function
   | PRef ref -> GRef (loc,ref)
   | PVar id -> GVar (loc,id)
-  | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (raw_of_pat env) l))
+  | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l))
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
@@ -862,26 +862,26 @@ let rec raw_of_pat env = function
   | PMeta None -> GHole (loc,Evd.InternalHole)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PApp (f,args) ->
-      GApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args)
+      GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args)
   | PSoApp (n,args) ->
       GApp (loc,GPatVar (loc,(true,n)),
-        List.map (raw_of_pat env) args)
+        List.map (glob_of_pat env) args)
   | PProd (na,t,c) ->
-      GProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
+      GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c)
   | PLetIn (na,t,c) ->
-      GLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
+      GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c)
   | PLambda (na,t,c) ->
-      GLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
+      GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c)
   | PIf (c,b1,b2) ->
-      GIf (loc, raw_of_pat env c, (Anonymous,None),
-           raw_of_pat env b1, raw_of_pat env b2)
+      GIf (loc, glob_of_pat env c, (Anonymous,None),
+           glob_of_pat env b1, glob_of_pat env b2)
   | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
-      let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
-      GLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+      let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in
+      GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b)
   | PCase (_,PMeta None,tm,[||]) ->
-      GCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
+      GCases (loc,RegularStyle,None,[glob_of_pat env tm,(Anonymous,None)],[])
   | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
-      let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
+      let brs = Array.to_list (Array.map (glob_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
         (* ind is None only if no branch and no return type *)
       let ind = Option.get indo in
@@ -890,14 +890,14 @@ let rec raw_of_pat env = function
 	if p = PMeta None then (Anonymous,None),None
 	else
 	  let nparams,n = Option.get ind_nargs in
-	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
-      GCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
+	  return_type_of_predicate ind nparams n (glob_of_pat env p) in
+      GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env pat =
-  extern true (None,[]) Idset.empty (raw_of_pat env pat)
+  extern true (None,[]) Idset.empty (glob_of_pat env pat)
 
 let extern_rel_context where env sign =
   let a = detype_rel_context where [] (names_of_rel_context env) sign in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 033090fc9e..e1fdd068b7 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -21,7 +21,7 @@ open Notation
 
 val check_same_type : constr_expr -> constr_expr -> unit
 
-(** Translation of pattern, cases pattern, rawterm and term into syntax
+(** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
 
 val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
@@ -36,7 +36,7 @@ val extern_constr : bool -> env -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
 val extern_reference : loc -> Idset.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
-val extern_sort : sorts -> rawsort
+val extern_sort : sorts -> glob_sort
 val extern_rel_context : constr option -> env ->
   rel_context -> local_binder list
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4e8d0a621a..1b3cedd778 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1134,17 +1134,17 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	     let n, ro, ((ids',_,_,_),rbl) =
 	       match order with
 	       | CStructRec ->
-		   intern_ro_arg (fun _ -> RStructRec)
+		   intern_ro_arg (fun _ -> GStructRec)
 	       | CWfRec c ->
-		   intern_ro_arg (fun f -> RWfRec (f c))
+		   intern_ro_arg (fun f -> GWfRec (f c))
 	       | CMeasureRec (m,r) ->
-		   intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
+		   intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
 	     in
 	     let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl,
              intern_type (ids',unb,tmp_scope,scopes) ty,
              intern (ids'',unb,None,scopes) bd)) dl in
-	GRec (loc,RFix
+	GRec (loc,GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
               Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -1166,7 +1166,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
             (List.rev rbl,
              intern_type (ids',unb,tmp_scope,scopes) ty,
              intern (ids'',unb,None,scopes) bd)) dl in
-	GRec (loc,RCoFix n,
+	GRec (loc,GCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
@@ -1504,7 +1504,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
   in
   let istype = kind = IsType in
   let c = intern_gen istype ~impls !evdref env c in
-  let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in
+  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
     Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
 
 let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 08839698a8..54aadba187 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -171,8 +171,8 @@ val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type
 val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type
 val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type
 
-val rawwit_sort : (rawsort,rlevel) abstract_argument_type
-val globwit_sort : (rawsort,glevel) abstract_argument_type
+val rawwit_sort : (glob_sort,rlevel) abstract_argument_type
+val globwit_sort : (glob_sort,glevel) abstract_argument_type
 val wit_sort : (sorts,tlevel) abstract_argument_type
 
 val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b430c000bf..428ddd6ab9 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -293,7 +293,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    CAppExpl (loc, (None, id), args), avoid
 	in c, avoid
 
-let implicits_of_rawterm ?(with_products=true) l =
+let implicits_of_glob_constr ?(with_products=true) l =
   let rec aux i c =
     let abs loc na bk t b =
       let rest = aux (succ i) b in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index cb782e0c51..05f54ec758 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -42,7 +42,7 @@ val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_rawterm : ?with_products:bool -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list
+val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 37c9ddbebf..86a5155374 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -176,7 +176,7 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 
-(* We define keys for rawterm and aconstr to split the syntax entries
+(* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
 type key =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 0e03268081..f8c0aeb870 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -44,7 +44,7 @@ type aconstr =
   | ARec of fix_kind * identifier array *
       (name * aconstr option * aconstr) list array * aconstr array *
       aconstr array
-  | ASort of rawsort
+  | ASort of glob_sort
   | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
@@ -552,8 +552,8 @@ let bind_binder (sigma,sigmalist,sigmabinders) x bl =
 
 let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with
-  | RCoFix n1, RCoFix n2 -> n1 = n2
-  | RFix (nl1,n1), RFix (nl2,n2) ->
+  | GCoFix n1, GCoFix n2 -> n1 = n2
+  | GFix (nl1,n1), GFix (nl2,n2) ->
       n1 = n2 &&
       array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
   | _ -> false
@@ -843,7 +843,7 @@ type constr_expr =
   | CHole of loc * Evd.hole_kind option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
-  | CSort of loc * rawsort
+  | CSort of loc * glob_sort
   | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_notation_substitution
   | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b01c35093d..405db2d172 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -41,7 +41,7 @@ type aconstr =
   | ARec of fix_kind * identifier array *
       (name * aconstr option * aconstr) list array * aconstr array *
       aconstr array
-  | ASort of rawsort
+  | ASort of glob_sort
   | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
@@ -158,7 +158,7 @@ type constr_expr =
   | CHole of loc * Evd.hole_kind option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
-  | CSort of loc * rawsort
+  | CSort of loc * glob_sort
   | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_notation_substitution
   | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr