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

8 files changed, 32 insertions, 32 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index c297f4965..0cc5af99f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -501,7 +501,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme (fas : (constant*Glob_term.rawsort) list) : Entries.definition_entry list =
+let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list =
   let env = Global.env ()
   and sigma = Evd.empty in
   let funs = List.map fst fas in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 24c8359dc..1c02c16ec 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 
 exception No_graph_found
 
-val make_scheme : (constant*Glob_term.rawsort) list -> Entries.definition_entry list
+val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list
 
-val build_scheme : (identifier*Libnames.reference*Glob_term.rawsort) list ->  unit
-val build_case_scheme : (identifier*Libnames.reference*Glob_term.rawsort)  ->  unit
+val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list ->  unit
+val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort)  ->  unit
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90f7b5970..fb053c032 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -167,7 +167,7 @@ END
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
   Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
   Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
-  Ppconstr.pr_rawsort s
+  Ppconstr.pr_glob_sort s
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
 PRINTED BY pr_fun_scheme_arg
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ce224d1aa..62cf3ccba 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1200,7 +1200,7 @@ let rec rebuild_return_type rt =
 	Topconstr.CArrow(loc,t,rebuild_return_type t')
     | Topconstr.CLetIn(loc,na,t,t') ->
 	Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
+    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,GType None))
 
 
 let do_build_inductive
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0cf91f38c..3fa1f6714 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -586,28 +586,28 @@ let id_of_name = function
   | Names.Name x -> x
 
 (* TODO: finish Rec caes *)
-let ids_of_rawterm c =
-  let rec ids_of_rawterm acc c =
+let ids_of_glob_constr c =
+  let rec ids_of_glob_constr acc c =
     let idof = id_of_name in
     match c with
       | GVar (_,id) -> id::acc
       | GApp (loc,g,args) ->
-          ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
-      | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
-      | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
-      | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
+          ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
+      | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
+      | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
+      | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
+      | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
+      | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc
+      | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
       | GLetTuple (_,nal,(na,po),b,c) ->
-          List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+          List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
       | GCases (loc,sty,rtntypopt,tml,brchl) ->
-	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
+	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
       | GRec _ -> failwith "Fix inside a constructor branch"
       | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> []
   in
   (* build the set *)
-  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)
+  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c)
 
 
 
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index b6c407a24..3afb86298 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -23,7 +23,7 @@ val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr
 val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr
 val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr
 val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
-val mkRSort : rawsort -> glob_constr
+val mkRSort : glob_sort -> glob_constr
 val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
 val mkRCast : glob_constr* glob_constr -> glob_constr
 (*
@@ -115,10 +115,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 val   ids_of_pat : cases_pattern -> Names.Idset.t
 
 (* TODO: finish this function (Fix not treated) *)
-val ids_of_rawterm: glob_constr -> Names.Idset.t
+val ids_of_glob_constr: glob_constr -> Names.Idset.t
 
 (*
-   removing let_in construction in a rawterm
+   removing let_in construction in a glob_constr
 *)
 val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4e5fb953d..426b496dd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -774,7 +774,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	       (fun entry ->
 		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
 	       )
-	       (make_scheme (array_map_to_list (fun const -> const,Glob_term.RType None) funs))
+	       (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs))
 	    )
     in
     let proving_tac =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 7c32c1d20..4eedf8dc2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -381,11 +381,11 @@ let build_raw_params prms_decl avoid =
   let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
   let res,_ = glob_decompose_prod dummy_glob_constr in
   let comblist = List.combine prms_decl res in
-  comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_glob_constr)))
+  comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr)))
 *)
 
 let ids_of_rawlist avoid rawl =
-    List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl)
+    List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl)
 
 
 
@@ -463,7 +463,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
       ([],[],[],[]) arity_ctxt in
 (*  let arity_ctxt2 =
     build_raw_params oib2.mind_arity_ctxt
-      (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*)
+      (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
   let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
   let _ = prstr "\n\n\n" in
   let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
@@ -756,7 +756,7 @@ let merge_constructor_id id1 id2 shift:identifier =
 
 
 (** [merge_constructors lnk shift avoid] merges the two list of
-    constructor [(name*type)]. These are translated to rawterms
+    constructor [(name*type)]. These are translated to glob_constr
     first, each of them having distinct var names. *)
 let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
     (typcstr1:(identifier * glob_constr) list)
@@ -816,7 +816,7 @@ let rec merge_mutual_inductive_body
   merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
 
 
-let rawterm_to_constr_expr x = (* build a constr_expr from a glob_constr *)
+let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
   Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x
 
 let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
@@ -827,7 +827,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prstr "param :" in
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
-        let typ = rawterm_to_constr_expr tp in
+        let typ = glob_constr_to_constr_expr tp in
         LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) concl in
@@ -844,18 +844,18 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
 
 
 
-(** [rawterm_list_to_inductive_expr ident rawlist] returns the
+(** [glob_constr_list_to_inductive_expr ident rawlist] returns the
     induct_expr corresponding to the the list of constructor types
     [rawlist], named ident.
     FIXME: params et cstr_expr (arity) *)
-let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
+let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     (rawlist:(identifier * glob_constr) list) =
   let lident = dummy_loc, shift.ident in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
   let lcstor_expr : (bool * (lident * constr_expr)) list  =
     List.map (* zeta_normalize t ? *)
-      (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
+      (fun (id,t) -> false, ((dummy_loc,id),glob_constr_to_constr_expr t))
       rawlist in
   lident , bindlist , Some cstr_expr , lcstor_expr
 
@@ -901,7 +901,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
       recprms1=prms1;
       recprms1=prms1;
     } in *)
-  let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
+  let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in