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

13 files changed, 56 insertions, 56 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 3a3f50ac8..a75f0e20b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -193,7 +193,7 @@ let abstract_one_hyp inject h raw =
 let glob_constr_of_hyps inject hyps head =
   List.fold_right (abstract_one_hyp inject) hyps head
 
-let raw_prop = GSort (dummy_loc,RProp Null)
+let glob_prop = GSort (dummy_loc,GProp Null)
 
 let rec match_hyps blend names constr = function
     [] -> [],substl names constr
@@ -214,7 +214,7 @@ let interp_hyps_gen inject blend sigma env hyps head =
   let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in
     match_hyps blend [] constr hyps
 
-let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps raw_prop)
+let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop)
 
 let dummy_prefix= id_of_string "__"
 
@@ -232,7 +232,7 @@ let rec deanonymize ids =
     | PatCstr(loc,cstr,lpat,nam) ->
 	PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
 
-let rec raw_of_pat =
+let rec glob_of_pat =
   function
       PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable"
     | PatVar (loc,Name id) ->
@@ -243,7 +243,7 @@ let rec raw_of_pat =
 	  if n<=0 then q else
 	    add_params (pred n) (GHole(dummy_loc,
 				       Evd.TomatchTypeParameter(ind,n))::q) in
-	    let args = List.map raw_of_pat lpat in
+	    let args = List.map glob_of_pat lpat in
 	      raw_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr),
 		   add_params mind.Declarations.mind_nparams args)
 
@@ -261,7 +261,7 @@ let prod_one_id (loc,id) raw =
 	 GHole (loc,Evd.BinderType (Name id)), raw)
 
 let let_in_one_alias (id,pat) raw =
-  GLetIn (dummy_loc,Name id, raw_of_pat pat, raw)
+  GLetIn (dummy_loc,Name id, glob_of_pat pat, raw)
 
 let rec bind_primary_aliases map pat =
   match pat with
@@ -343,22 +343,22 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
       raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
-      Thesis (Plain) -> Glob_term.GSort(dummy_loc,RProp Null)
+      Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null)
     | Thesis (For rec_occ) ->
 	if not (List.mem rec_occ pat_vars) then
 	  errorlabstrm "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
-	Glob_term.GSort(dummy_loc,RProp Null)
+	Glob_term.GSort(dummy_loc,GProp Null)
     | This (c,_) -> c in
-  let term1 = glob_constr_of_hyps inject hyps raw_prop in
+  let term1 = glob_constr_of_hyps inject hyps glob_prop in
   let loc_ids,npatt =
     let rids=ref ([],pat_vars) in
     let npatt= deanonymize rids patt in
       List.rev (fst !rids),npatt in
   let term2 =
     GLetIn(dummy_loc,Anonymous,
-	   GCast(dummy_loc,raw_of_pat npatt,
+	   GCast(dummy_loc,glob_of_pat npatt,
 		 CastConv (DEFAULTcast,app_ind)),term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
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
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 27f2292e3..41d92b233 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -470,7 +470,7 @@ Just testing ...
 #use "include.ml";;
 open Quote;;
 
-let r = raw_constr_of_string;;
+let r = glob_constr_of_string;;
 
 let ivs = {
   normal_lhs_rhs =
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 4dfdc5875..4f8344745 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -155,22 +155,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/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index c7924261a..7c0d12325 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -114,14 +114,14 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon =
       | Some t ->
 	  let t = Topconstr.prod_constr_expr t bl in
 	  let t = coqintern_type !isevars env t in
-	  let imps = Implicit_quantifiers.implicits_of_rawterm t in
+	  let imps = Implicit_quantifiers.implicits_of_glob_constr t in
 	  let coqt, ttyp = interp env isevars t empty_tycon in
 	    mk_tycon coqt, Some imps
   in
   let c = coqintern_constr !isevars env c in
   let imps = match imps with 
     | Some i -> i
-    | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c
+    | None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c
   in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars !isevars in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index b1c4101ce..28bf6e64d 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -160,8 +160,8 @@ module SubtacPretyping_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 ()
 
   let split_tycon_lam loc env evd tycon =
     let rec real_split evd c =
@@ -216,7 +216,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | GPatVar (loc,(someta,n)) ->
-	anomaly "Found a pattern variable in a rawterm to type"
+	anomaly "Found a pattern variable in a glob_constr to type"
 
     | GHole (loc,k) ->
 	let ty =
@@ -257,7 +257,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    push_rec_types (names,marked_ftys,[||]) env
 	in
-	let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
+	let fixi = match fixkind with GFix (vn, i) -> i | GCoFix i -> i in
 	let vdefj =
 	  array_map2_i
 	    (fun i ctxt def ->
@@ -284,7 +284,7 @@ module SubtacPretyping_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,
@@ -300,7 +300,7 @@ module SubtacPretyping_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