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

3 files changed, 14 insertions, 14 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 4dfdc58754..4f8344745e 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 c7924261af..7c0d123259 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 b1c4101cea..28bf6e64d0 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