Change of nomenclature: rawconstr -> glob_constr

There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.

In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.

The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.

This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):

perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 48 insertions, 48 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 62fa0b2c9f..0ea2290db8 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -88,7 +88,7 @@ let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
 
-let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
 
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index b6a42b6b46..5ef6f0f881 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -86,7 +86,7 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
 type rhs =
     { rhs_env    : env;
       avoid_ids  : identifier list;
-      it         : rawconstr;
+      it         : glob_constr;
     }
 
 type equation =
@@ -234,7 +234,7 @@ type pattern_matching_problem =
       mat      : matrix;
       caseloc  : loc;
       casestyle: case_style;
-      typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
+      typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -366,10 +366,10 @@ let find_tomatch_tycon isevars env loc = function
   | None -> empty_tycon
 
 let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
-  let loc = Some (loc_of_rawconstr tomatch) in
+  let loc = Some (loc_of_glob_constr tomatch) in
   let tycon = find_tomatch_tycon isevars env loc indopt in
   let j = typing_fun tycon env tomatch in
-  let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
+  let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in
   isevars := evd;
   let typ = nf_evar ( !isevars) j.uj_type in
   let t =
@@ -527,7 +527,7 @@ let extract_rhs pb =
 let occur_in_rhs na rhs =
   match na with
     | Anonymous -> false
-    | Name id -> occur_rawconstr id rhs.it
+    | Name id -> occur_glob_constr id rhs.it
 
 let is_dep_patt eqn = function
   | PatVar (_,name) -> occur_in_rhs name eqn.rhs
@@ -1515,7 +1515,7 @@ let mk_JMeq typ x typ' y =
   mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
 
-let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
+let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
 let constr_of_pat env isevars arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
@@ -1604,12 +1604,12 @@ let vars_of_ctx ctx =
       match b with
 	| Some t' when kind_of_term t' = Rel 0 ->
 	    prev,
-	    (RApp (dummy_loc,
-		(RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+	    (GApp (dummy_loc,
+		(GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars
 	| _ ->
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
-	      | Name n -> n, RVar (dummy_loc, n) :: vars)
+	      | Name n -> n, GVar (dummy_loc, n) :: vars)
       ctx (id_of_string "vars_of_ctx_error", [])
   in List.rev y
 
@@ -1741,13 +1741,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
-	   let bref = RVar (dummy_loc, branch_name) in
+	   let bref = GVar (dummy_loc, branch_name) in
 	     match vars_of_ctx rhs_rels with
 		 [] -> bref
-	       | l -> RApp (dummy_loc, bref, l)
+	       | l -> GApp (dummy_loc, bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> RApp (dummy_loc, branch, [ hole ])
+	     Some _ -> GApp (dummy_loc, branch, [ hole ])
 	   | None -> branch
 	 in
 	 incr i;
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 8527766305..24fdd679b3 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -84,16 +84,16 @@ let interp_constr_judgment isevars env c =
     { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
 
 let locate_if_isevar loc na = function
-  | RHole _ ->
+  | GHole _ ->
       (try match na with
-	| Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id)
+	| Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> RHole (loc, Evd.BinderType na))
+      with Not_found -> GHole (loc, Evd.BinderType na))
   | x -> x
 
 let interp_binder sigma env na t =
   let t = Constrintern.intern_gen true ( !sigma) env t in
-    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
 
 let interp_context_evars evdref env params =
   let bl = Constrintern.intern_context false !evdref env params in
@@ -102,7 +102,7 @@ let interp_context_evars evdref env params =
       (fun (env,params,n,impls) (na, k, b, t) ->
 	match b with
 	    None ->
-	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
 	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
 	      let d = (na,None,t) in
 	      let impls =
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 2eb7408aae..09cc17328c 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -58,7 +58,7 @@ let my_print_rec_info env t =
   str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
   str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
   str "Full type: " ++ my_print_constr env t.f_fulltype
-(*   trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
+(*   trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *)
 (* 	   str " and tycon "++ my_print_tycon env tycon ++ *)
 (* 	   str " in environment: " ++ my_print_env env); *)
 
@@ -81,9 +81,9 @@ let find_with_index x l =
 
 open Vernacexpr
 
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.glob_constr = 
   Constrintern.intern_constr evd env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.glob_constr = 
   Constrintern.intern_type evd env
 
 let env_with_binders env isevars l =
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 48906b23cf..2b0c8fda28 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -13,7 +13,7 @@ module Pretyping : Pretyping.S
 val interp :
     Environ.env ->
     Evd.evar_map ref ->
-    Rawterm.rawconstr ->
+    Rawterm.glob_constr ->
     Evarutil.type_constraint -> Term.constr * Term.constr
 
 val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 3d79508c3a..debd4f0532 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -189,22 +189,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   (* in environment [env], with existential variables [( evdref)] and *)
   (* the type constraint tycon *)
   let rec pretype (tycon : type_constraint) env evdref lvar c =
-(*     let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
+(*     let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *)
 (* 			       str " with tycon " ++ Evarutil.pr_tycon env tycon)  *)
 (*     with _ -> () *)
 (*     in *)
     match c with
-    | RRef (loc,ref) ->
+    | GRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_ref evdref env ref)
 	  tycon
 
-    | RVar (loc, id) ->
+    | GVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
-    | REvar (loc, ev, instopt) ->
+    | GEvar (loc, ev, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
 	let hyps = evar_context (Evd.find !evdref ev) in
@@ -215,10 +215,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let j = (Retyping.get_judgment_of env !evdref c) in
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
-    | RPatVar (loc,(someta,n)) ->
+    | GPatVar (loc,(someta,n)) ->
 	anomaly "Found a pattern variable in a rawterm to type"
 
-    | RHole (loc,k) ->
+    | GHole (loc,k) ->
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
@@ -226,7 +226,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | RRec (loc,fixkind,names,bl,lar,vdef) ->
+    | GRec (loc,fixkind,names,bl,lar,vdef) ->
 	let rec type_bl env ctxt = function
             [] -> ctxt
           | (na,k,None,ty)::bl ->
@@ -306,10 +306,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
-    | RSort (loc,s) ->
+    | GSort (loc,s) ->
 	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
 
-    | RApp (loc,f,args) ->
+    | GApp (loc,f,args) ->
 	let length = List.length args in
 	let ftycon =
 	  let ty =
@@ -326,11 +326,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | _ -> None
 	in
 	let fj = pretype ftycon env evdref lvar f in
- 	let floc = loc_of_rawconstr f in
+ 	let floc = loc_of_glob_constr f in
 	let rec apply_rec env n resj tycon = function
 	  | [] -> resj
 	  | c::rest ->
-	      let argloc = loc_of_rawconstr c in
+	      let argloc = loc_of_glob_constr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
               let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
@@ -364,7 +364,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  | _ -> resj in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLambda(loc,name,k,c1,c2)      ->
+    | GLambda(loc,name,k,c1,c2)      ->
 	let tycon' = evd_comb1
 	  (fun evd tycon ->
 	    match tycon with
@@ -382,7 +382,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let resj = judge_of_abstraction env name j j' in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RProd(loc,name,k,c1,c2)        ->
+    | GProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let var = (name,j.utj_val) in
 	let env' = Termops.push_rel_assum var env in
@@ -392,7 +392,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  with TypeError _ as e -> Loc.raise loc e in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLetIn(loc,name,c1,c2)      ->
+    | GLetIn(loc,name,c1,c2)      ->
 	let j = pretype empty_tycon env evdref lvar c1 in
 	let t = Termops.refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
@@ -401,12 +401,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	    uj_type = subst1 j.uj_val j'.uj_type }
 
-    | RLetTuple (loc,nal,(na,po),c,d) ->
+    | GLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
 	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
+	    let cloc = loc_of_glob_constr c in
 	      error_case_not_inductive_loc cloc env !evdref cj
 	in
 	let cstrs = get_constructors env indf in
@@ -466,12 +466,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     in
 		       { uj_val = v; uj_type = ccl })
 
-    | RIf (loc,c,(na,po),b1,b2) ->
+    | GIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
 	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
+	    let cloc = loc_of_glob_constr c in
 	      error_case_not_inductive_loc cloc env !evdref cj in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 2 then
@@ -536,12 +536,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
-    | RCases (loc,sty,po,tml,eqns) ->
+    | GCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast (loc,c,k) ->
+    | GCast (loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
@@ -557,7 +557,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	in
 	  inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | RDynamic (loc,d) ->
+    | GDynamic (loc,d) ->
 	if (Dyn.tag d) = "constr" then
 	  let c = constr_out d in
 	  let j = (Retyping.get_judgment_of env !evdref c) in
@@ -568,7 +568,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
-    | RHole loc ->
+    | GHole loc ->
 	(match valcon with
 	   | Some v ->
                let s =
@@ -588,7 +588,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		   utj_type = s})
     | c ->
 	let j = pretype empty_tycon env evdref lvar c in
-	let loc = loc_of_rawconstr c in
+	let loc = loc_of_glob_constr c in
 	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	  match valcon with
 	    | None -> tj
@@ -596,7 +596,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env evdref v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env !evdref tj.utj_val v
+                    (loc_of_glob_constr c) env !evdref tj.utj_val v
 
   let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 106ac4d091..43b55ca95f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -116,7 +116,7 @@ let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
 let my_print_context = Termops.print_rel_context
 let my_print_named_context = Termops.print_named_context
 let my_print_env = Termops.print_env
-let my_print_rawconstr = Printer.pr_rawconstr_env
+let my_print_glob_constr = Printer.pr_glob_constr_env
 let my_print_evardefs = Evd.pr_evar_map
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index f56c2932e5..659a677812 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -74,7 +74,7 @@ val my_print_context : env -> std_ppcmds
 val my_print_rel_context : env -> rel_context -> std_ppcmds
 val my_print_named_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds
-val my_print_rawconstr : env -> rawconstr -> std_ppcmds
+val my_print_glob_constr : env -> glob_constr -> std_ppcmds
 val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds