Rename mkR* smart constructors (mostly in funind)

perl -pi -e 's/(mk)R(Ref|Var|Evar|PatVar|App|Lambda|Prod|LetIn|Case
s|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic|Prop|Type|Fix|CoFix|Struct
Rec|WfRec|MeasureRec)/\1G\2/g' **/*.ml*

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

5 files changed, 69 insertions, 69 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1b3cedd77..8454b8fef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -293,14 +293,14 @@ let set_type_scope (ids,unb,tmp_scope,scopes) =
 let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
   (ids,unb,None,scopes)
 
-let rec it_mkRProd env body =
+let rec it_mkGProd env body =
   match env with
-      (na, bk, _, t) :: tl -> it_mkRProd tl (GProd (dummy_loc, na, bk, t, body))
+      (na, bk, _, t) :: tl -> it_mkGProd tl (GProd (dummy_loc, na, bk, t, body))
     | [] -> body
 
-let rec it_mkRLambda env body =
+let rec it_mkGLambda env body =
   match env with
-      (na, bk, _, t) :: tl -> it_mkRLambda tl (GLambda (dummy_loc, na, bk, t, body))
+      (na, bk, _, t) :: tl -> it_mkGLambda tl (GLambda (dummy_loc, na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -1356,7 +1356,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	| Generalized (b,b',t) ->
 	    let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
 	    let body = intern_type env body in
-	      it_mkRProd ibind body
+	      it_mkGProd ibind body
 
   and iterate_lam loc2 env bk ty body nal =
     let rec default env bk = function
@@ -1371,7 +1371,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
       | Generalized (b, b', t) ->
 	  let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
 	  let body = intern env body in
-	    it_mkRLambda ibind body
+	    it_mkGLambda ibind body
 
   and intern_impargs c env l subscopes args =
     let l = select_impargs_size (List.length args) l in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 62cf3ccba..394417abb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -33,9 +33,9 @@ type glob_context = (binder_type*glob_constr) list
 let compose_glob_context =
   let compose_binder  (bt,t) acc =
     match bt with
-      | Lambda n -> mkRLambda(n,t,acc)
-      | Prod n -> mkRProd(n,t,acc)
-      | LetIn n -> mkRLetIn(n,t,acc)
+      | Lambda n -> mkGLambda(n,t,acc)
+      | Prod n -> mkGProd(n,t,acc)
+      | LetIn n -> mkGLetIn(n,t,acc)
   in
   List.fold_right compose_binder
 
@@ -160,7 +160,7 @@ let apply_args ctxt body args =
 	  (ctxt,body)
       | [],_ -> (* no more fun *)
 	  let f,args' = glob_decompose_app body in
-	  (ctxt,mkRApp(f,args'@args))
+	  (ctxt,mkGApp(f,args'@args))
       | (Lambda Anonymous,t)::ctxt',arg::args' ->
 	  do_apply avoid ctxt' body args'
       | (Lambda (Name id),t)::ctxt',arg::args' ->
@@ -215,7 +215,7 @@ let combine_app f args =
 let combine_lam n t b =
   {
     context = [];
-    value = mkRLambda(n, compose_glob_context t.context t.value,
+    value = mkGLambda(n, compose_glob_context t.context t.value,
 		      compose_glob_context b.context b.value )
   }
 
@@ -269,8 +269,8 @@ let make_discr_match_brl i =
   list_map_i
     (fun j (_,idl,patl,_) ->
        if j=i
-       then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref))
-       else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref))
+       then (dummy_loc,idl,patl, mkGRef (Lazy.force coq_True_ref))
+       else (dummy_loc,idl,patl, mkGRef (Lazy.force coq_False_ref))
     )
     0
 (*
@@ -281,7 +281,7 @@ let make_discr_match_brl i =
 *)
 let make_discr_match brl =
   fun el i ->
-  mkRCases(None,
+  mkGCases(None,
 	   make_discr_match_el el,
 	   make_discr_match_brl i brl)
 
@@ -312,12 +312,12 @@ let build_constructors_of_type ind' argl =
 		  if argl = []
 		  then
  		    Array.to_list
-		      (Array.init (cst_narg - npar) (fun _ -> mkRHole ())
+		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
 		      )
 		  else argl
 		in
 		let pat_as_term =
-		  mkRApp(mkRRef (ConstructRef(ind',i+1)),argl)
+		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
 		in
 		cases_pattern_of_glob_constr Anonymous pat_as_term
 	     )
@@ -419,7 +419,7 @@ let add_pat_variables pat typ env : Environ.env =
 let rec pattern_to_term_and_type env typ  = function
   | PatVar(loc,Anonymous) -> assert false
   | PatVar(loc,Name id) ->
-	mkRVar id
+	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
 	Inductiveops.mis_constructor_nargs_env
@@ -445,7 +445,7 @@ let rec pattern_to_term_and_type env typ  = function
       let patl_as_term =
 	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
       in
-      mkRApp(mkRRef(ConstructRef constr),
+      mkGApp(mkGRef(ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
@@ -525,13 +525,13 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
 		let res = fresh_id args_res.to_avoid "res" in
 		let new_avoid = res::args_res.to_avoid in
-		let res_rt = mkRVar res in
+		let res_rt = mkGVar res in
 		let new_result =
 		  List.map
 		    (fun arg_res ->
 		       let new_hyps =
 			 [Prod (Name res),res_raw_type;
-			  Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
+			  Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)]
 		       in
 		       {context =  arg_res.context@new_hyps; value = res_rt }
 		    )
@@ -549,7 +549,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		    result =
 		    List.map
 		      (fun args_res ->
-			 {args_res with value = mkRApp(f,args_res.value)})
+			 {args_res with value = mkGApp(f,args_res.value)})
 		      args_res.result
 		}
 	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
@@ -577,7 +577,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		  env
 		  funnames
 		  avoid
-		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
+		  (mkGLetIn(new_n,t,mkGApp(new_b,args)))
 	    | GCases _  | GIf _ | GLetTuple _ ->
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and
@@ -592,7 +592,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 
 		   WARNING: We need to restart since [b] itself should be an application term
 		*)
-		build_entry_lc env funnames avoid (mkRApp(b,args))
+		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> error "Not handled GRec"
 	    | GProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *)
@@ -663,7 +663,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	    [lhs;rhs]
 	in
 	let match_expr =
-	  mkRCases(None,[(b,(Anonymous,None))],brl)
+	  mkGCases(None,[(b,(Anonymous,None))],brl)
 	in
 	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
 	build_entry_lc env funnames avoid match_expr
@@ -672,8 +672,8 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let nal_as_glob_constr =
 	    List.map
 	      (function
-		   Name id -> mkRVar id
-		 | Anonymous -> mkRHole ()
+		   Name id -> mkGVar id
+		 | Anonymous -> mkGHole ()
 	      )
 	      nal
 	  in
@@ -691,7 +691,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let br =
 	    (dummy_loc,[],[case_pats.(0)],e)
 	  in
-	  let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
 	  build_entry_lc env funnames avoid match_expr
 
 	end
@@ -778,7 +778,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			  Detyping.detype false []
 			    (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
 			in
-			mkRProd (Name id,raw_typ_of_id,acc))
+			mkGProd (Name id,raw_typ_of_id,acc))
 		     pat_ids
 		     (glob_make_neq pat'_as_term (pattern_to_term renamed_pat))
 	    )
@@ -901,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			  i*)
 
 			let new_t =
-			  mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt])
+			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
 			let t' = Pretyping.Default.understand Evd.empty env new_t in
 			let new_env = Environ.push_rel (n,None,t') env in
@@ -911,7 +911,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    args new_crossed_types
 			    (depth + 1) b
 			in
-			mkRProd(n,new_t,new_b),
+			mkGProd(n,new_t,new_b),
 			Idset.filter not_free_in_t id_to_exclude
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
@@ -942,7 +942,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			new_args new_crossed_types
 			(depth + 1) subst_b
 		    in
-		    mkRProd(n,t,new_b),id_to_exclude
+		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
 		    let jmeq = Libnames.IndRef (destInd (jmeq ())) in
 		    let ty' = Pretyping.Default.understand Evd.empty env ty in
@@ -961,7 +961,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				 p) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
-					 (mkRHole ()))))
+					 (mkGHole ()))))
 		    in
 		    let eq' =
 		      GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
@@ -1025,11 +1025,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			new_args new_crossed_types
 			(depth + 1) subst_b
 		    in
-		    mkRProd(n,eq',new_b),id_to_exclude
+		    mkGProd(n,eq',new_b),id_to_exclude
 		end
 		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
 		     if keep_eq then
-		     mkRProd(n,t,new_b),id_to_exclude
+		     mkGProd(n,t,new_b),id_to_exclude
 		     else new_b, Idset.add id id_to_exclude
 		  *)
 	    | _ ->
@@ -1046,7 +1046,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
 		      new_b,Idset.remove id
 			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	end
     | GLambda(_,n,k,t,b) ->
 	begin
@@ -1060,7 +1060,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
-		    (args@[mkRVar id])new_crossed_types
+		    (args@[mkGVar id])new_crossed_types
 		    (depth + 1 ) b
 		in
 		if Idset.mem id id_to_exclude && depth >= nb_args
@@ -1117,7 +1117,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 
 	end
 
-    | _ -> mkRApp(mkRVar  relname,args@[rt]),Idset.empty
+    | _ -> mkGApp(mkGVar  relname,args@[rt]),Idset.empty
 
 
 (* debuging wrapper *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 3fa1f6714..0de1104e7 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -9,16 +9,16 @@ let idmap_is_empty m = m = Idmap.empty
    Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-let mkRRef ref = GRef(dummy_loc,ref)
-let mkRVar id = GVar(dummy_loc,id)
-let mkRApp(rt,rtl) = GApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b)
-let mkRProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b)
-let mkRLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b)
-let mkRCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl)
-let mkRSort s = GSort(dummy_loc,s)
-let mkRHole () = GHole(dummy_loc,Evd.BinderType Anonymous)
-let mkRCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
+let mkGRef ref = GRef(dummy_loc,ref)
+let mkGVar id = GVar(dummy_loc,id)
+let mkGApp(rt,rtl) = GApp(dummy_loc,rt,rtl)
+let mkGLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b)
+let mkGProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b)
+let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b)
+let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl)
+let mkGSort s = GSort(dummy_loc,s)
+let mkGHole () = GHole(dummy_loc,Evd.BinderType Anonymous)
+let mkGCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
 
 (*
   Some basic functions to decompose glob_constrs
@@ -43,14 +43,14 @@ let glob_decompose_prod_or_letin =
   glob_decompose_prod []
 
 let glob_compose_prod =
-  List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
+  List.fold_left (fun b (n,t) -> mkGProd(n,t,b))
 
 let glob_compose_prod_or_letin =
   List.fold_left (
       fun concl decl ->
 	match decl with
-	  | (n,None,Some t) -> mkRProd(n,t,concl)
-	  | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl)
+	  | (n,None,Some t) -> mkGProd(n,t,concl)
+	  | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl)
 	  | _ -> assert false)
 
 let glob_decompose_prod_n n =
@@ -93,15 +93,15 @@ let glob_decompose_app =
 
 
 (* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *)
-let glob_make_eq ?(typ= mkRHole ()) t1 t2  =
-  mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
+let glob_make_eq ?(typ= mkGHole ()) t1 t2  =
+  mkGApp(mkGRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
 
 (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
 let glob_make_neq t1 t2 =
-  mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2])
+  mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2])
 
 (* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
-let glob_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
+let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
 
 (* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
    to [P1 \/ ( .... \/ Pn)]
@@ -425,7 +425,7 @@ let is_free_in id =
 let rec pattern_to_term  = function
   | PatVar(loc,Anonymous) -> assert false
   | PatVar(loc,Name id) ->
-	mkRVar id
+	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
 	Inductiveops.mis_constructor_nargs_env
@@ -436,13 +436,13 @@ let rec pattern_to_term  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun _ -> mkRHole ())
+	     (fun _ -> mkGHole ())
 	  )
       in
       let patl_as_term =
 	List.map pattern_to_term patternl
       in
-      mkRApp(mkRRef(Libnames.ConstructRef constr),
+      mkGApp(mkGRef(Libnames.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 3afb86298..bfd153579 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -16,16 +16,16 @@ val pattern_to_term : cases_pattern -> glob_constr
    Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-val mkRRef : Libnames.global_reference -> glob_constr
-val mkRVar : Names.identifier -> glob_constr
-val mkRApp  : glob_constr*(glob_constr list) -> glob_constr
-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 : glob_sort -> glob_constr
-val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
-val mkRCast : glob_constr* glob_constr -> glob_constr
+val mkGRef : Libnames.global_reference -> glob_constr
+val mkGVar : Names.identifier -> glob_constr
+val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
+val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr
+val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr
+val mkGLetIn : Names.name * glob_constr * glob_constr -> glob_constr
+val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
+val mkGSort : glob_sort -> glob_constr
+val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
+val mkGCast : glob_constr* glob_constr -> glob_constr
 (*
   Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 50dd413c6..ae86f3142 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -285,8 +285,8 @@ let rec pat_of_raw metas vars = function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (loc,nal,(_,None),b,c) ->
-      let mkRLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in
-      let c = List.fold_left mkRLambda c nal in
+      let mkGLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in
+      let c = List.fold_left mkGLambda c nal in
       PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
              [|pat_of_raw metas vars c|])
   | GCases (loc,sty,p,[c,(na,indnames)],brs) ->