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

9 files changed, 431 insertions, 431 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9c3982cb5..b2b4145d7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -125,12 +125,12 @@ let functional_induction with_clean c princl pat =
     Dumpglob.continue ();
     res
 
-let rec abstract_rawconstr c = function
+let rec abstract_glob_constr c = function
   | [] -> c
-  | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
+  | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl)
   | Topconstr.LocalRawAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
-        (abstract_rawconstr c bl)
+        (abstract_glob_constr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen false sigma env ~impls
@@ -161,7 +161,7 @@ let build_newrecursive
       try
 	List.map
 	  (fun (_,bl,_,def)  ->
-             let def = abstract_rawconstr def bl in
+             let def = abstract_glob_constr def bl in
              interp_casted_constr_with_implicits
 	       sigma rec_sign rec_impls def
 	  )
@@ -188,15 +188,15 @@ let rec is_rec names =
   let names = List.fold_right Idset.add names Idset.empty in
   let check_id id names =  Idset.mem id names in
   let rec lookup names = function
-    | RVar(_,id) -> check_id id names
-    | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
-    | RCast(_,b,_) -> lookup names b
-    | RRec _ -> error "RRec not handled"
-    | RIf(_,b,_,lhs,rhs) ->
+    | GVar(_,id) -> check_id id names
+    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GDynamic _ -> false
+    | GCast(_,b,_) -> lookup names b
+    | GRec _ -> error "GRec not handled"
+    | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  ->
+    | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b)  ->
 	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
-    | RLetTuple(_,nal,_,t,b) -> lookup names t ||
+    | GLetTuple(_,nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
 	     (fun acc na -> Nameops.name_fold Idset.remove na acc)
@@ -204,8 +204,8 @@ let rec is_rec names =
 	     nal
 	  )
 	  b
-    | RApp(_,f,args) -> List.exists (lookup names) (f::args)
-    | RCases(_,_,_,el,brl) ->
+    | GApp(_,f,args) -> List.exists (lookup names) (f::args)
+    | GCases(_,_,_,el,brl) ->
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
   and lookup_br names (_,idl,_,rt) =
@@ -222,7 +222,7 @@ let rec local_binders_length = function
 
 let prepare_body ((name,_,args,types,_),_) rt =
   let n = local_binders_length args in
-(*   Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *)
+(*   Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *)
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 002fb7098..9db361cf5 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -76,8 +76,8 @@ let chop_rlambda_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
-	  | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+	  | Rawterm.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+	  | Rawterm.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ ->
 	      raise (Util.UserError("chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
@@ -90,7 +90,7 @@ let chop_rprod_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	  | Rawterm.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
 	  | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index c48dff0c6..d802ecf2b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -35,11 +35,11 @@ val list_union_eq :
 val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
-val chop_rlambda_n : int -> Rawterm.rawconstr ->
-  (name*Rawterm.rawconstr*bool) list * Rawterm.rawconstr
+val chop_rlambda_n : int -> Rawterm.glob_constr ->
+  (name*Rawterm.glob_constr*bool) list * Rawterm.glob_constr
 
-val chop_rprod_n : int -> Rawterm.rawconstr ->
-  (name*Rawterm.rawconstr) list * Rawterm.rawconstr
+val chop_rprod_n : int -> Rawterm.glob_constr ->
+  (name*Rawterm.glob_constr) list * Rawterm.glob_constr
 
 val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 7c460f7d3..ed8cb9cb6 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -25,7 +25,7 @@ open Rawtermops
 
 (** {1 Utilities}  *)
 
-(** {2 Useful operations on constr and rawconstr} *)
+(** {2 Useful operations on constr and glob_constr} *)
 
 let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
 
@@ -60,7 +60,7 @@ let string_of_name nme = string_of_id (id_of_name nme)
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
     match x with
-      | RVar (_,x) -> Pervasives.compare x f = 0
+      | GVar (_,x) -> Pervasives.compare x f = 0
       | _ -> false
 
 (** [ident_global_exist id] returns true if identifier [id] is linked
@@ -97,7 +97,7 @@ let prNamedConstr s c =
 let prNamedRConstr s c =
   begin
     msg(str "");
-    msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} ");
+    msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} ");
     msg(str "");
   end
 let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
@@ -377,11 +377,11 @@ let verify_inds mib1 mib2 =
 let build_raw_params prms_decl avoid =
   let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in
   let _ = prNamedConstr "DUMMY" dummy_constr in
-  let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
-  let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in
-  let res,_ = raw_decompose_prod dummy_rawconstr in
+  let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in
+  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_rawconstr)))
+  comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_glob_constr)))
 *)
 
 let ids_of_rawlist avoid rawl =
@@ -511,37 +511,37 @@ exception NoMerge
 let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
   match c1 , c2 with
-    | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
+    | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
         let _ = prstr "\nICI1!\n";Pp.flush_all() in
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args)
-    | RApp(_,f1, arr1), RApp(_,f2,arr2)  -> raise NoMerge
-    | RLetIn(_,nme,bdy,trm) , _ ->
+        GApp (dummy_loc,GVar (dummy_loc,shift.ident) , args)
+    | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
+    | GLetIn(_,nme,bdy,trm) , _ ->
         let _ = prstr "\nICI2!\n";Pp.flush_all() in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
-        RLetIn(dummy_loc,nme,bdy,newtrm)
-    | _, RLetIn(_,nme,bdy,trm) ->
+        GLetIn(dummy_loc,nme,bdy,newtrm)
+    | _, GLetIn(_,nme,bdy,trm) ->
         let _ = prstr "\nICI3!\n";Pp.flush_all() in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        RLetIn(dummy_loc,nme,bdy,newtrm)
+        GLetIn(dummy_loc,nme,bdy,newtrm)
     | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
            raise NoMerge
 
 let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
   match c1 , c2 with
-    | RApp(_,f1, arr1), RApp(_,f2,arr2) ->
+    | GApp(_,f1, arr1), GApp(_,f2,arr2) ->
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args)
+        GApp (dummy_loc,GVar(dummy_loc,shift.ident) , args)
           (* FIXME: what if the function appears in the body of the let? *)
-    | RLetIn(_,nme,bdy,trm) , _ ->
+    | GLetIn(_,nme,bdy,trm) , _ ->
         let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        RLetIn(dummy_loc,nme,bdy,newtrm)
-    | _, RLetIn(_,nme,bdy,trm) ->
+        GLetIn(dummy_loc,nme,bdy,newtrm)
+    | _, GLetIn(_,nme,bdy,trm) ->
         let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        RLetIn(dummy_loc,nme,bdy,newtrm)
+        GLetIn(dummy_loc,nme,bdy,newtrm)
     | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
 
 
@@ -550,24 +550,24 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
    calls of branch 1 with all rec calls of branch 2. *)
 (* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
 let rec merge_rec_hyps shift accrec
-    (ltyp:(Names.name * rawconstr option * rawconstr option) list)
-    filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list =
+    (ltyp:(Names.name * glob_constr option * glob_constr option) list)
+    filter_shift_stable : (Names.name * glob_constr option * glob_constr option) list =
   let mergeonehyp t reldecl =
     match reldecl with
-      | (nme,x,Some (RApp(_,i,args) as ind))
+      | (nme,x,Some (GApp(_,i,args) as ind))
         -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
       | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
       | (nme,None,Some _) -> assert false
       | (nme,None,None) | (nme,Some _,Some _) -> assert false in
   match ltyp with
     | [] -> []
-    | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
+    | (nme,None,Some (GApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
         let rechyps = List.map (mergeonehyp t) accrec in
         rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
     | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
 
 
-let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift =
+let rec build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
   List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
 
 
@@ -577,7 +577,7 @@ let find_app (nme:identifier) ltyp =
       (List.map
           (fun x ->
             match x with
-              | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+              | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0)
               | _ -> ())
           ltyp);
     false
@@ -591,9 +591,9 @@ let prnt_prod_or_letin nm letbdy typ =
 
 
 let rec merge_types shift accrec1
-    (ltyp1:(name * rawconstr option * rawconstr option) list)
-    (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2
-    : (name * rawconstr option * rawconstr option) list * rawconstr =
+    (ltyp1:(name * glob_constr option * glob_constr option) list)
+    (concl1:glob_constr) (ltyp2:(name * glob_constr option * glob_constr option) list) concl2
+    : (name * glob_constr option * glob_constr option) list * glob_constr =
   let _ = prstr "MERGE_TYPES\n" in
   let _ = prstr "ltyp 1 : " in
   let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
@@ -637,7 +637,7 @@ let rec merge_types shift accrec1
           rechyps , concl
       | (nme,None, Some t1)as e ::lt1 ->
           (match t1 with
-            | RApp(_,f,carr) when isVarf ind1name f ->
+            | GApp(_,f,carr) when isVarf ind1name f ->
                 merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
             | _ ->
                 let recres, recconcl2 =
@@ -704,8 +704,8 @@ let build_link_map allargs1 allargs2 lnk =
     Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint.
 
     TODO: return nothing if equalities (after linking) are contradictory. *)
-let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
-    (typcstr2:rawconstr) : rawconstr =
+let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr)
+    (typcstr2:glob_constr) : glob_constr =
   (* FIXME: les noms des parametres corerspondent en principe au
      parametres du niveau mib, mais il faudrait s'en assurer *)
   (* shift.nfunresprmsx last args are functional result *)
@@ -713,17 +713,17 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
     shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in
   let nargs2 =
     shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in
-  let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in
-  let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in
+  let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in
+  let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in
   (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
   let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
   let rest2 = change_vars linked_map rest2 in
-  let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in
-  let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in
+  let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in
+  let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in
   let ltyp,concl2 =
     merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
   let _ = prNamedRLDecl "ltyp result:" ltyp in
-  let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in
+  let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in
   let revargs1 =
     list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
   let _ = prNamedRLDecl "ltyp allargs1" allargs1 in
@@ -733,7 +733,7 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
   let _ = prNamedRLDecl "ltyp allargs2" allargs2 in
   let _ = prNamedRLDecl "ltyp revargs2" revargs2 in
   let typwithprms =
-    raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
+    glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
   typwithprms
 
 
@@ -759,8 +759,8 @@ let merge_constructor_id id1 id2 shift:identifier =
     constructor [(name*type)]. These are translated to rawterms
     first, each of them having distinct var names. *)
 let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
-    (typcstr1:(identifier * rawconstr) list)
-    (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list =
+    (typcstr1:(identifier * glob_constr) list)
+    (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list =
   List.flatten
     (List.map
         (fun (id1,rawtyp1) ->
@@ -778,12 +778,12 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
     info in [shift], avoiding identifiers in [avoid]. *)
 let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
     (oib2:one_inductive_body) =
-  (* building rawconstr type of constructors *)
+  (* building glob_constr type of constructors *)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
     Detyping.detype false (Idset.elements avoid) [] substindtyp in
-  let lcstr1: rawconstr list =
+  let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
   let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in
@@ -792,10 +792,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in
 
   let params1 =
-    try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
+    try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
     with _ -> [] in
   let params2 =
-    try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
+    try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
     with _ -> [] in
 
   let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
@@ -816,8 +816,8 @@ 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 rawconstr *)
-  Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x
+let rawterm_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) =
   let params = prms2 @ prms1 in
@@ -849,7 +849,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     [rawlist], named ident.
     FIXME: params et cstr_expr (arity) *)
 let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
-    (rawlist:(identifier * rawconstr) list) =
+    (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
@@ -861,21 +861,21 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
 
 
 
-let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
+let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
         let traw = Detyping.detype false [] [] t in
-        RProd (dummy_loc,nme,Explicit,traw,t2)
+        GProd (dummy_loc,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
 
 
-let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
+let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
         let traw = Detyping.detype false [] [] t in
-        RProd (dummy_loc,nme,Explicit,traw,t2)
+        GProd (dummy_loc,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index f8da96bdf..7b67e20f3 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -23,14 +23,14 @@ type binder_type =
   | Prod of name
   | LetIn of name
 
-type raw_context = (binder_type*rawconstr) list
+type glob_context = (binder_type*glob_constr) list
 
 (*
-   compose_raw_context [(bt_1,n_1,t_1);......] rt returns
+   compose_glob_context [(bt_1,n_1,t_1);......] rt returns
    b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
    binders corresponding to the bt_i's
 *)
-let compose_raw_context =
+let compose_glob_context =
   let compose_binder  (bt,t) acc =
     match bt with
       | Lambda n -> mkRLambda(n,t,acc)
@@ -47,7 +47,7 @@ let compose_raw_context =
 
 type 'a build_entry_pre_return =
     {
-      context : raw_context;  (* the binding context of the result *)
+      context : glob_context;  (* the binding context of the result *)
       value : 'a; (* The value *)
     }
 
@@ -159,7 +159,7 @@ let apply_args ctxt body args =
       | _,[] -> (* No more args *)
 	  (ctxt,body)
       | [],_ -> (* no more fun *)
-	  let f,args' = raw_decompose_app body in
+	  let f,args' = glob_decompose_app body in
 	  (ctxt,mkRApp(f,args'@args))
       | (Lambda Anonymous,t)::ctxt',arg::args' ->
 	  do_apply avoid ctxt' body args'
@@ -215,8 +215,8 @@ let combine_app f args =
 let combine_lam n t b =
   {
     context = [];
-    value = mkRLambda(n, compose_raw_context t.context t.value,
-		      compose_raw_context b.context b.value )
+    value = mkRLambda(n, compose_glob_context t.context t.value,
+		      compose_glob_context b.context b.value )
   }
 
 
@@ -319,15 +319,15 @@ let build_constructors_of_type ind' argl =
 		let pat_as_term =
 		  mkRApp(mkRRef (ConstructRef(ind',i+1)),argl)
 		in
-		cases_pattern_of_rawconstr Anonymous pat_as_term
+		cases_pattern_of_glob_constr Anonymous pat_as_term
 	     )
     ind.Declarations.mind_consnames
 
 (* [find_type_of] very naive attempts to discover the type of an if or a letin *)
 let rec find_type_of nb b =
-  let f,_ = raw_decompose_app b in
+  let f,_ = glob_decompose_app b in
   match f with
-    | RRef(_,ref) ->
+    | GRef(_,ref) ->
 	begin
 	  let ind_type  =
 	    match ref with
@@ -350,8 +350,8 @@ let rec find_type_of nb b =
 	  then raise (Invalid_argument "find_type_of : not a valid inductive");
 	  ind_type
 	end
-    | RCast(_,b,_) -> find_type_of nb b
-    | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
+    | GCast(_,b,_) -> find_type_of nb b
+    | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *)
     | _ -> raise (Invalid_argument "not a ref")
 
 
@@ -472,7 +472,7 @@ let rec pattern_to_term_and_type env typ  = function
    and concatenate them (informally, each branch of a match produces a new constructor)
    \end{itemize}
 
-   WARNING: The terms constructed here are only USING the rawconstr syntax but are highly bad formed.
+   WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed.
    We must wait to have complete all the current calculi to set the recursive calls.
    At this point, each term [f t1 ... tn]  (where f appears in [funnames]) is replaced by
    a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later.
@@ -481,15 +481,15 @@ let rec pattern_to_term_and_type env typ  = function
 *)
 
 
-let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
-  observe (str " Entering : " ++ Printer.pr_rawconstr rt);
+let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
+  observe (str " Entering : " ++ Printer.pr_glob_constr rt);
   match rt with
-    | RRef _ | RVar _ | REvar _ | RPatVar _     | RSort _  | RHole _  ->
+    | GRef _ | GVar _ | GEvar _ | GPatVar _     | GSort _  | GHole _  ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
-    | RApp(_,_,_) ->
-	let f,args = raw_decompose_app rt in
-	let args_res : (rawconstr list) build_entry_return =
+    | GApp(_,_,_) ->
+	let f,args = glob_decompose_app rt in
+	let args_res : (glob_constr list) build_entry_return =
 	  List.fold_right (* create the arguments lists of constructors and combine them *)
 	    (fun arg ctxt_argsl ->
 	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
@@ -500,19 +500,19 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	in
 	begin
 	  match f with
-	    | RLambda _  -> 
+	    | GLambda _  -> 
 		let rec aux t l = 
 		  match l with 
 		    | [] -> t
 		    | u::l -> 
 			match t with 
-			  | RLambda(loc,na,_,nat,b) -> 
-			      RLetIn(dummy_loc,na,u,aux b l)
+			  | GLambda(loc,na,_,nat,b) -> 
+			      GLetIn(dummy_loc,na,u,aux b l)
 			  | _ -> 
-			      RApp(dummy_loc,t,l)
+			      GApp(dummy_loc,t,l)
 		in
 		build_entry_lc env funnames avoid (aux f args)
-	    | RVar(_,id) when Idset.mem id funnames ->
+	    | GVar(_,id) when Idset.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
 		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
@@ -538,7 +538,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		    args_res.result
 		in
 		{ result = new_result; to_avoid = new_avoid }
-	    | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ ->
+	    | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
 		(* if have [g t1 ... tn] with [g] not appearing in [funnames]
 		   then
 		   foreach [ctxt,v1 ... vn] in [args_res] we return
@@ -552,8 +552,8 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 			 {args_res with value = mkRApp(f,args_res.value)})
 		      args_res.result
 		}
-	    | RApp _ -> assert false (* we have collected all the app in [raw_decompose_app] *)
-       	    | RLetIn(_,n,t,b) ->
+	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
+       	    | GLetIn(_,n,t,b) ->
 		(* if we have [(let x := v in b) t1 ... tn] ,
 		   we discard our work and compute the list of constructor for
 		   [let x = v in (b t1 ... tn)] up to alpha conversion
@@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (RVar(dummy_loc,id))
+			    (GVar(dummy_loc,id))
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -578,26 +578,26 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		  funnames
 		  avoid
 		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
-	    | RCases _  | RIf _ | RLetTuple _ ->
+	    | GCases _  | GIf _ | GLetTuple _ ->
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and
 		   then combine each of them with each of args one
 		*)
 		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
-	    | RDynamic _ ->error "Not handled RDynamic"
-	    | RCast(_,b,_) ->
+	    | GDynamic _ ->error "Not handled GDynamic"
+	    | GCast(_,b,_) ->
 		(* for an applied cast we just trash the cast part
 		   and restart the work.
 
 		   WARNING: We need to restart since [b] itself should be an application term
 		*)
 		build_entry_lc env funnames avoid (mkRApp(b,args))
-	    | RRec _ -> error "Not handled RRec"
-	    | RProd _ -> error "Cannot apply a type"
+	    | GRec _ -> error "Not handled GRec"
+	    | GProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *)
 
-    | RLambda(_,n,_,t,b) ->
+    | GLambda(_,n,_,t,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the type
@@ -612,7 +612,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	let new_env = raw_push_named (new_n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
-    | RProd(_,n,_,t,b) ->
+    | GProd(_,n,_,t,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the type
@@ -622,7 +622,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	let new_env = raw_push_named (n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_prod n) t_res b_res
-    | RLetIn(_,n,v,b) ->
+    | GLetIn(_,n,v,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the value [t]
@@ -638,21 +638,21 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
-    | RCases(_,_,_,el,brl) ->
+    | GCases(_,_,_,el,brl) ->
 	(* we create the discrimination function
 	   and treat the case itself
 	*)
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
-    | RIf(_,b,(na,e_option),lhs,rhs) ->
+    | GIf(_,b,(na,e_option),lhs,rhs) ->
 	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
 	let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env Evd.empty b_typ
 	  with Not_found ->
 	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
-			       Printer.pr_rawconstr b ++ str " in " ++
-			       Printer.pr_rawconstr rt ++ str ". try again with a cast")
+			       Printer.pr_glob_constr b ++ str " in " ++
+			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
 	let case_pats = build_constructors_of_type ind [] in
 	assert (Array.length case_pats = 2);
@@ -665,11 +665,11 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	let match_expr =
 	  mkRCases(None,[(b,(Anonymous,None))],brl)
 	in
-	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
+	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
 	build_entry_lc env funnames avoid match_expr
-    | RLetTuple(_,nal,_,b,e) ->
+    | GLetTuple(_,nal,_,b,e) ->
 	begin
-	  let nal_as_rawconstr =
+	  let nal_as_glob_constr =
 	    List.map
 	      (function
 		   Name id -> mkRVar id
@@ -683,10 +683,10 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	    try Inductiveops.find_inductive env Evd.empty b_typ
 	    with Not_found ->
 	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
-				 Printer.pr_rawconstr b ++ str " in " ++
-				 Printer.pr_rawconstr rt ++ str ". try again with a cast")
+				 Printer.pr_glob_constr b ++ str " in " ++
+				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
-	  let case_pats = build_constructors_of_type ind nal_as_rawconstr in
+	  let case_pats = build_constructors_of_type ind nal_as_glob_constr in
 	  assert (Array.length case_pats = 1);
 	  let br =
 	    (dummy_loc,[],[case_pats.(0)],e)
@@ -695,14 +695,14 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	  build_entry_lc env funnames avoid match_expr
 
 	end
-    | RRec _ -> error "Not handled RRec"
-    | RCast(_,b,_) ->
+    | GRec _ -> error "Not handled GRec"
+    | GCast(_,b,_) ->
 	build_entry_lc env funnames  avoid b
-    | RDynamic _ -> error "Not handled RDynamic"
+    | GDynamic _ -> error "Not handled GDynamic"
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
     (brl:Rawterm.cases_clauses) avoid :
-    rawconstr build_entry_return =
+    glob_constr build_entry_return =
   match el with
     | [] -> assert false (* this case correspond to match <nothing> with .... !*)
     | el ->
@@ -762,7 +762,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	   (will be used in the following recursive calls)
 	*)
 	let new_env = List.fold_right2 add_pat_variables patl types env in
-	let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list =
+	let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list =
 	  List.map2
 	    (fun pat typ ->
 	       fun avoid pat'_as_term ->
@@ -780,7 +780,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			in
 			mkRProd (Name id,raw_typ_of_id,acc))
 		     pat_ids
-		     (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
+		     (glob_make_neq pat'_as_term (pattern_to_term renamed_pat))
 	    )
 	    patl
 	    types
@@ -835,7 +835,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      else acc
 		   )
 		   idl
-		   [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
+		   [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)]
 	      )
 	      patl
 	      matched_expr.value
@@ -883,18 +883,18 @@ exception Continue
    eliminates some meaningless equalities, applies some rewrites......
 *)
 let rec rebuild_cons env nb_args relname args crossed_types depth rt =
-  observe (str "rebuilding : " ++ pr_rawconstr rt);
+  observe (str "rebuilding : " ++ pr_glob_constr rt);
 
   match rt with
-    | RProd(_,n,k,t,b) ->
+    | GProd(_,n,k,t,b) ->
 	let not_free_in_t id = not (is_free_in id t) in
 	let new_crossed_types = t::crossed_types in
 	begin
 	  match t with
-	    | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id ->
+	    | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id ->
 		begin
 		  match args' with
-		    | (RVar(_,this_relname))::args' ->
+		    | (GVar(_,this_relname))::args' ->
 			(*i The next call to mk_rel_id is
 			  valid since we are constructing the graph
 			  Ensures by: obvious
@@ -916,12 +916,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
-	    | RApp(loc1,RRef(loc2,eq_as_ref),[ty;RVar(loc3,id);rt])
+	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
 		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
 		  ->
 		begin
 		  try
-		    observe (str "computing new type for eq : " ++ pr_rawconstr rt);
+		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
 		      try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue
 		    in
@@ -953,8 +953,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      ((Util.list_chop nparam args'))
 		    in
 		    let rt_typ =
-		       RApp(Util.dummy_loc,
-			    RRef (Util.dummy_loc,Libnames.IndRef ind),
+		       GApp(Util.dummy_loc,
+			    GRef (Util.dummy_loc,Libnames.IndRef ind),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 (Termops.names_of_rel_context env)
@@ -964,9 +964,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkRHole ()))))
 		    in
 		    let eq' =
-		      RApp(loc1,RRef(loc2,jmeq),[ty;RVar(loc3,id);rt_typ;rt])
+		      GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
 		    in
-		    observe (str "computing new type for jmeq : " ++ pr_rawconstr eq');
+		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
 		    let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
@@ -1033,7 +1033,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     else new_b, Idset.add id id_to_exclude
 		  *)
 	    | _ ->
-		observe (str "computing new type for prod : " ++ pr_rawconstr rt);
+		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
 		let t' = Pretyping.Default.understand Evd.empty env t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
@@ -1048,11 +1048,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			(Idset.filter not_free_in_t id_to_exclude)
 		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	end
-    | RLambda(_,n,k,t,b) ->
+    | GLambda(_,n,k,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
-	  observe (str "computing new type for lambda : " ++ pr_rawconstr rt);
+	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
 	  let t' = Pretyping.Default.understand Evd.empty env t in
 	  match n with
 	    | Name id ->
@@ -1067,12 +1067,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		then
 		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
 		else
-		  RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly "Should not have an anonymous function here"
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
-    | RLetIn(_,n,t,b) ->
+    | GLetIn(_,n,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let t' = Pretyping.Default.understand Evd.empty env t in
@@ -1086,10 +1086,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | 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)
-	    | _ -> RLetIn(dummy_loc,n,t,new_b),
+	    | _ -> GLetIn(dummy_loc,n,t,new_b),
 		Idset.filter not_free_in_t id_to_exclude
 	end
-    | RLetTuple(_,nal,(na,rto),t,b) ->
+    | GLetTuple(_,nal,(na,rto),t,b) ->
 	assert (rto=None);
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
@@ -1112,7 +1112,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 (* 	    | Name id when Idset.mem id id_to_exclude ->  *)
 (* 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  RLetTuple(dummy_loc,nal,(na,None),t,new_b),
+	  GLetTuple(dummy_loc,nal,(na,None),t,new_b),
 		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
 
 	end
@@ -1122,12 +1122,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 
 (* debuging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
-(*   observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++  *)
+(*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
 (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
   let res =
     rebuild_cons env nb_args relname args crossed_types 0 rt
   in
-(*   observe (str " leads to "++ pr_rawconstr (fst res)); *)
+(*   observe (str " leads to "++ pr_glob_constr (fst res)); *)
   res
 
 
@@ -1139,30 +1139,30 @@ let rebuild_cons env nb_args relname args crossed_types rt =
    TODO: Find a valid way to deal with implicit arguments here!
 *)
 let rec compute_cst_params relnames params = function
-  | RRef _ | RVar _ | REvar _ | RPatVar _ -> params
-  | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+  | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
+  | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames ->
       compute_cst_params_from_app [] (params,rtl)
-  | RApp(_,f,args) ->
+  | GApp(_,f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
+  | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) ->
       let t_params = compute_cst_params relnames params t in
       compute_cst_params relnames t_params b
-  | RCases _ ->
+  | GCases _ ->
       params  (* If there is still cases at this point they can only be
 		 discriminitation ones *)
-  | RSort _ -> params
-  | RHole _ -> params
-  | RIf _ | RRec _ | RCast _ | RDynamic _  ->
+  | GSort _ -> params
+  | GHole _ -> params
+  | GIf _ | GRec _ | GCast _ | GDynamic _  ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,is_defined) as param)::params',(RVar(_,id'))::rtl'
+    | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl'
 	when id_ord id id' == 0 && not is_defined ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
-let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) list array) csts =
+let compute_params_name relnames (args : (Names.name * Rawterm.glob_constr * bool) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
@@ -1181,7 +1181,7 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool)
 	   if array_for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
-		n = n' && Topconstr.eq_rawconstr nt nt' && is_defined = is_defined')
+		n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined')
 	     rels_params
 	   then
 	     l := param::!l
@@ -1204,11 +1204,11 @@ let rec rebuild_return_type rt =
 
 
 let do_build_inductive
-    funnames (funsargs: (Names.name * rawconstr * bool) list list)
+    funnames (funsargs: (Names.name * glob_constr * bool) list list)
     returned_types
-    (rtl:rawconstr list) =
+    (rtl:glob_constr list) =
   let _time1 = System.get_time () in
-(*   Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *)
+(*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
   let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
   let funnames = Array.of_list funnames in
   let funsargs = Array.of_list funsargs in
@@ -1233,19 +1233,19 @@ let do_build_inductive
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-      let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list  =
+      let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list  =
 	funargs
       in
       List.fold_right
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t,
+	     Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
 			      acc)
 	   else
 	     Topconstr.CProdN
 	       (dummy_loc,
-		[[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
+		[[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
 		acc
 	       )
 	)
@@ -1264,9 +1264,9 @@ let do_build_inductive
   let constr i res =
     List.map
       (function result (* (args',concl') *) ->
-	 let rt = compose_raw_context result.context result.value in
+	 let rt = compose_glob_context result.context result.value in
 	 let nb_args = List.length funsargs.(i) in
-	 (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_rawconstr rt)) rt; *)
+	 (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
 	 fst (
 	   rebuild_cons env_with_graphs nb_args relnames.(i)
 	     []
@@ -1285,7 +1285,7 @@ let do_build_inductive
       i*)
     id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
   in
-  let rel_constructors i rt : (identifier*rawconstr) list =
+  let rel_constructors i rt : (identifier*glob_constr) list =
     next_constructor_id := (-1);
     List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
   in
@@ -1299,19 +1299,19 @@ let do_build_inductive
     rel_constructors
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list  =
+    let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list  =
       (snd (list_chop nrel_params funargs))
     in
     List.fold_right
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t,
+	   Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
 			    acc)
 	 else
 	   Topconstr.CProdN
 	   (dummy_loc,
-	   [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
+	   [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
 	    acc
 	   )
       )
@@ -1328,10 +1328,10 @@ let do_build_inductive
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t)
+	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t)
 	 else
 	 Topconstr.LocalRawAssum
-	   ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t)
+	   ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
       )
       rels_params
   in
@@ -1341,7 +1341,7 @@ let do_build_inductive
 	 false,((dummy_loc,id),
 		Flags.with_option
 		  Flags.raw_print
-		  (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
+		  (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t)
 	       )
       ))
       (rel_constructors)
diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli
index a314050f7..772e422f8 100644
--- a/plugins/funind/rawterm_to_relation.mli
+++ b/plugins/funind/rawterm_to_relation.mli
@@ -9,8 +9,8 @@
 
 val build_inductive :
   Names.identifier list -> (* The list of function name *)
-  (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
+  (Names.name*Rawterm.glob_constr*bool) list list -> (* The list of function args *)
   Topconstr.constr_expr list -> (* The list of function returned type *)
-  Rawterm.rawconstr list -> (* the list of body *)
+  Rawterm.glob_constr list -> (* the list of body *)
   unit
 
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index e31f1452d..f372fb017 100644
--- a/plugins/funind/rawtermops.ml
+++ b/plugins/funind/rawtermops.ml
@@ -6,46 +6,46 @@ open Names
 let idmap_is_empty m = m = Idmap.empty
 
 (*
-   Some basic functions to rebuild rawconstr
+   Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-let mkRRef ref = RRef(dummy_loc,ref)
-let mkRVar id = RVar(dummy_loc,id)
-let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
-let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
-let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
-let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl)
-let mkRSort s = RSort(dummy_loc,s)
-let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
+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))
 
 (*
-  Some basic functions to decompose rawconstrs
+  Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
-let raw_decompose_prod =
-  let rec raw_decompose_prod args = function
-  | RProd(_,n,k,t,b) ->
-      raw_decompose_prod ((n,t)::args) b
+let glob_decompose_prod =
+  let rec glob_decompose_prod args = function
+  | GProd(_,n,k,t,b) ->
+      glob_decompose_prod ((n,t)::args) b
   | rt -> args,rt
   in
-  raw_decompose_prod []
-
-let raw_decompose_prod_or_letin =
-  let rec raw_decompose_prod args = function
-  | RProd(_,n,k,t,b) ->
-      raw_decompose_prod ((n,None,Some t)::args) b
-  | RLetIn(_,n,t,b) ->
-      raw_decompose_prod ((n,Some t,None)::args) b
+  glob_decompose_prod []
+
+let glob_decompose_prod_or_letin =
+  let rec glob_decompose_prod args = function
+  | GProd(_,n,k,t,b) ->
+      glob_decompose_prod ((n,None,Some t)::args) b
+  | GLetIn(_,n,t,b) ->
+      glob_decompose_prod ((n,Some t,None)::args) b
   | rt -> args,rt
   in
-  raw_decompose_prod []
+  glob_decompose_prod []
 
-let raw_compose_prod =
+let glob_compose_prod =
   List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
 
-let raw_compose_prod_or_letin =
+let glob_compose_prod_or_letin =
   List.fold_left (
       fun concl decl ->
 	match decl with
@@ -53,37 +53,37 @@ let raw_compose_prod_or_letin =
 	  | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl)
 	  | _ -> assert false)
 
-let raw_decompose_prod_n n =
-  let rec raw_decompose_prod i args c =
+let glob_decompose_prod_n n =
+  let rec glob_decompose_prod i args c =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,_,t,b) ->
-	    raw_decompose_prod (i-1) ((n,t)::args) b
+	| GProd(_,n,_,t,b) ->
+	    glob_decompose_prod (i-1) ((n,t)::args) b
 	| rt -> args,rt
   in
-  raw_decompose_prod n []
+  glob_decompose_prod n []
 
 
-let raw_decompose_prod_or_letin_n n =
-  let rec raw_decompose_prod i args c =
+let glob_decompose_prod_or_letin_n n =
+  let rec glob_decompose_prod i args c =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,_,t,b) ->
-	    raw_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| RLetIn(_,n,t,b) ->
-	    raw_decompose_prod (i-1) ((n,Some t,None)::args) b
+	| GProd(_,n,_,t,b) ->
+	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
+	| GLetIn(_,n,t,b) ->
+	    glob_decompose_prod (i-1) ((n,Some t,None)::args) b
 	| rt -> args,rt
   in
-  raw_decompose_prod n []
+  glob_decompose_prod n []
 
 
-let raw_decompose_app =
+let glob_decompose_app =
   let rec decompose_rapp acc rt =
-(*     msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
+(*     msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
     match rt with
-    | RApp(_,rt,rtl) ->
+    | GApp(_,rt,rtl) ->
 	decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
     | rt -> rt,List.rev acc
   in
@@ -92,24 +92,24 @@ let raw_decompose_app =
 
 
 
-(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-let raw_make_eq ?(typ= mkRHole ()) t1 t2  =
+(* [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])
 
-(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
-let raw_make_neq t1 t2 =
-  mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2])
+(* [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])
 
-(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
-let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[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])
 
-(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
+(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
    to [P1 \/ ( .... \/ Pn)]
 *)
-let rec raw_make_or_list = function
+let rec glob_make_or_list = function
   | [] -> raise (Invalid_argument "mk_or")
   | [e] -> e
-  | e::l -> raw_make_or e (raw_make_or_list l)
+  | e::l -> glob_make_or e (glob_make_or_list l)
 
 
 let remove_name_from_mapping mapping na =
@@ -120,70 +120,70 @@ let remove_name_from_mapping mapping na =
 let change_vars =
   let rec change_vars mapping rt =
     match rt with
-      | RRef _ -> rt
-      | RVar(loc,id) ->
+      | GRef _ -> rt
+      | GVar(loc,id) ->
 	  let new_id =
 	    try
 	      Idmap.find id mapping
 	    with Not_found -> id
 	  in
-	  RVar(loc,new_id)
-      | REvar _ -> rt
-      | RPatVar _ -> rt
-      | RApp(loc,rt',rtl) ->
-	  RApp(loc,
+	  GVar(loc,new_id)
+      | GEvar _ -> rt
+      | GPatVar _ -> rt
+      | GApp(loc,rt',rtl) ->
+	  GApp(loc,
 	       change_vars mapping rt',
 	       List.map (change_vars mapping) rtl
 	      )
-      | RLambda(loc,name,k,t,b) ->
-	  RLambda(loc,
+      | GLambda(loc,name,k,t,b) ->
+	  GLambda(loc,
 		  name,
 		  k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | RProd(loc,name,k,t,b) ->
-	  RProd(loc,
+      | GProd(loc,name,k,t,b) ->
+	  GProd(loc,
 		  name,
 	          k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | RLetIn(loc,name,def,b) ->
-	  RLetIn(loc,
+      | GLetIn(loc,name,def,b) ->
+	  GLetIn(loc,
 		 name,
 		 change_vars mapping def,
 		 change_vars (remove_name_from_mapping mapping name) b
 		)
-      | RLetTuple(loc,nal,(na,rto),b,e) ->
+      | GLetTuple(loc,nal,(na,rto),b,e) ->
 	  let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
-	  RLetTuple(loc,
+	  GLetTuple(loc,
 		    nal,
 		    (na, Option.map (change_vars mapping) rto),
 		    change_vars mapping b,
 		    change_vars new_mapping e
 		   )
-      | RCases(loc,sty,infos,el,brl) ->
-	  RCases(loc,sty,
+      | GCases(loc,sty,infos,el,brl) ->
+	  GCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (change_vars mapping e,x)) el,
 		 List.map (change_vars_br mapping) brl
 		)
-      | RIf(loc,b,(na,e_option),lhs,rhs) ->
-	  RIf(loc,
+      | GIf(loc,b,(na,e_option),lhs,rhs) ->
+	  GIf(loc,
 	      change_vars mapping b,
 	      (na,Option.map (change_vars mapping) e_option),
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
-      | RRec _ -> error "Local (co)fixes are not supported"
-      | RSort _ -> rt
-      | RHole _ -> rt
-      | RCast(loc,b,CastConv (k,t)) ->
-	  RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
-      | RCast(loc,b,CastCoerce) ->
-	  RCast(loc,change_vars mapping b,CastCoerce)
-      | RDynamic _ -> error "Not handled RDynamic"
+      | GRec _ -> error "Local (co)fixes are not supported"
+      | GSort _ -> rt
+      | GHole _ -> rt
+      | GCast(loc,b,CastConv (k,t)) ->
+	  GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
+      | GCast(loc,b,CastCoerce) ->
+	  GCast(loc,change_vars mapping b,CastCoerce)
+      | GDynamic _ -> error "Not handled GDynamic"
   and change_vars_br mapping ((loc,idl,patl,res) as br) =
     let new_mapping = List.fold_right Idmap.remove idl mapping in
     if idmap_is_empty new_mapping
@@ -262,22 +262,22 @@ let get_pattern_id pat = raw_get_pattern_id pat []
 let rec alpha_rt excluded rt =
   let new_rt =
     match rt with
-      | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
-      | RLambda(loc,Anonymous,k,t,b) ->
+      | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
+      | GLambda(loc,Anonymous,k,t,b) ->
 	  let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
-	  RLambda(loc,Name new_id,k,new_t,new_b)
-      | RProd(loc,Anonymous,k,t,b) ->
+	  GLambda(loc,Name new_id,k,new_t,new_b)
+      | GProd(loc,Anonymous,k,t,b) ->
 	let new_t = alpha_rt excluded t in
 	let new_b = alpha_rt excluded b in
-	RProd(loc,Anonymous,k,new_t,new_b)
-    | RLetIn(loc,Anonymous,t,b) ->
+	GProd(loc,Anonymous,k,new_t,new_b)
+    | GLetIn(loc,Anonymous,t,b) ->
 	let new_t = alpha_rt excluded t in
 	let new_b = alpha_rt excluded b in
-	RLetIn(loc,Anonymous,new_t,new_b)
-    | RLambda(loc,Name id,k,t,b) ->
+	GLetIn(loc,Anonymous,new_t,new_b)
+    | GLambda(loc,Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if new_id = id
@@ -289,8 +289,8 @@ let rec alpha_rt excluded rt =
 	let new_excluded = new_id::excluded in
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	RLambda(loc,Name new_id,k,new_t,new_b)
-    | RProd(loc,Name id,k,t,b) ->
+	GLambda(loc,Name new_id,k,new_t,new_b)
+    | GProd(loc,Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let new_excluded = new_id::excluded in
 	let t,b =
@@ -302,8 +302,8 @@ let rec alpha_rt excluded rt =
 	in
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	RProd(loc,Name new_id,k,new_t,new_b)
-    | RLetIn(loc,Name id,t,b) ->
+	GProd(loc,Name new_id,k,new_t,new_b)
+    | GLetIn(loc,Name id,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if new_id = id
@@ -315,10 +315,10 @@ let rec alpha_rt excluded rt =
 	let new_excluded = new_id::excluded in
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	RLetIn(loc,Name new_id,new_t,new_b)
+	GLetIn(loc,Name new_id,new_t,new_b)
 
 
-    | RLetTuple(loc,nal,(na,rto),t,b) ->
+    | GLetTuple(loc,nal,(na,rto),t,b) ->
 	let rev_new_nal,new_excluded,mapping =
 	  List.fold_left
 	    (fun (nal,excluded,mapping) na ->
@@ -345,28 +345,28 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt new_excluded new_t in
 	let new_b = alpha_rt new_excluded new_b in
 	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
-	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
-    | RCases(loc,sty,infos,el,brl) ->
+	GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
+    | GCases(loc,sty,infos,el,brl) ->
 	let new_el =
 	  List.map (function (rt,i) -> alpha_rt excluded rt, i) el
 	in
-	RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl)
-    | RIf(loc,b,(na,e_o),lhs,rhs) ->
-	RIf(loc,alpha_rt excluded b,
+	GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl)
+    | GIf(loc,b,(na,e_o),lhs,rhs) ->
+	GIf(loc,alpha_rt excluded b,
 	    (na,Option.map (alpha_rt excluded) e_o),
 	    alpha_rt excluded lhs,
 	    alpha_rt excluded rhs
 	   )
-    | RRec _ -> error "Not handled RRec"
-    | RSort _ -> rt
-    | RHole _ -> rt
-    | RCast (loc,b,CastConv (k,t)) ->
-	RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
-    | RCast (loc,b,CastCoerce) ->
-	RCast(loc,alpha_rt excluded b,CastCoerce)
-    | RDynamic _ -> error "Not handled RDynamic"
-    | RApp(loc,f,args) ->
-	RApp(loc,
+    | GRec _ -> error "Not handled GRec"
+    | GSort _ -> rt
+    | GHole _ -> rt
+    | GCast (loc,b,CastConv (k,t)) ->
+	GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
+    | GCast (loc,b,CastCoerce) ->
+	GCast(loc,alpha_rt excluded b,CastCoerce)
+    | GDynamic _ -> error "Not handled GDynamic"
+    | GApp(loc,f,args) ->
+	GApp(loc,
 	     alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
 	    )
@@ -386,35 +386,35 @@ and alpha_br excluded (loc,ids,patl,res) =
 *)
 let is_free_in id =
   let rec is_free_in = function
-    | RRef _ ->  false
-    | RVar(_,id') -> id_ord id' id == 0
-    | REvar _ -> false
-    | RPatVar _ -> false
-    | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
+    | GRef _ ->  false
+    | GVar(_,id') -> id_ord id' id == 0
+    | GEvar _ -> false
+    | GPatVar _ -> false
+    | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
+    | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> id_ord id' id <> 0
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
-    | RCases(_,_,_,el,brl) ->
+    | GCases(_,_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
-    | RLetTuple(_,nal,_,b,t) ->
+    | GLetTuple(_,nal,_,b,t) ->
 	let check_in_nal =
 	  not (List.exists (function Name id' -> id'= id | _ -> false) nal)
 	in
 	is_free_in t  || (check_in_nal && is_free_in b)
 
-    | RIf(_,cond,_,br1,br2) ->
+    | GIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
-    | RRec _ -> raise (UserError("",str "Not handled RRec"))
-    | RSort _ -> false
-    | RHole _ -> false
-    | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
-    | RCast (_,b,CastCoerce) -> is_free_in b
-    | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+    | GRec _ -> raise (UserError("",str "Not handled GRec"))
+    | GSort _ -> false
+    | GHole _ -> false
+    | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
+    | GCast (_,b,CastCoerce) -> is_free_in b
+    | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and is_free_in_br (_,ids,_,rt) =
     (not (List.mem id ids)) && is_free_in rt
   in
@@ -451,69 +451,69 @@ let rec pattern_to_term  = function
 let replace_var_by_term x_id term =
   let rec replace_var_by_pattern rt =
     match rt with
-      | RRef _ -> rt
-      | RVar(_,id) when id_ord id x_id == 0 -> term
-      | RVar _ -> rt
-      | REvar _ -> rt
-      | RPatVar _ -> rt
-      | RApp(loc,rt',rtl) ->
-	  RApp(loc,
+      | GRef _ -> rt
+      | GVar(_,id) when id_ord id x_id == 0 -> term
+      | GVar _ -> rt
+      | GEvar _ -> rt
+      | GPatVar _ -> rt
+      | GApp(loc,rt',rtl) ->
+	  GApp(loc,
 	       replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
-      | RLambda(loc,name,k,t,b) ->
-	  RLambda(loc,
+      | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | GLambda(loc,name,k,t,b) ->
+	  GLambda(loc,
 		  name,
 		  k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
-      | RProd(loc,name,k,t,b) ->
-	  RProd(loc,
+      | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | GProd(loc,name,k,t,b) ->
+	  GProd(loc,
 		  name,
 	          k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RLetIn(loc,name,def,b) ->
-	  RLetIn(loc,
+      | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+      | GLetIn(loc,name,def,b) ->
+	  GLetIn(loc,
 		 name,
 		 replace_var_by_pattern def,
 		 replace_var_by_pattern b
 		)
-      | RLetTuple(_,nal,_,_,_)
+      | GLetTuple(_,nal,_,_,_)
 	  when List.exists (function Name id -> id = x_id | _ -> false) nal  ->
 	  rt
-      | RLetTuple(loc,nal,(na,rto),def,b) ->
-	  RLetTuple(loc,
+      | GLetTuple(loc,nal,(na,rto),def,b) ->
+	  GLetTuple(loc,
 		    nal,
 		    (na,Option.map replace_var_by_pattern rto),
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
-      | RCases(loc,sty,infos,el,brl) ->
-	  RCases(loc,sty,
+      | GCases(loc,sty,infos,el,brl) ->
+	  GCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
 		 List.map replace_var_by_pattern_br brl
 		)
-      | RIf(loc,b,(na,e_option),lhs,rhs) ->
-	  RIf(loc, replace_var_by_pattern b,
+      | GIf(loc,b,(na,e_option),lhs,rhs) ->
+	  GIf(loc, replace_var_by_pattern b,
 	      (na,Option.map replace_var_by_pattern e_option),
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
-      | RRec _ -> raise (UserError("",str "Not handled RRec"))
-      | RSort _ -> rt
-      | RHole _ -> rt
-      | RCast(loc,b,CastConv(k,t)) ->
-	  RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
-      | RCast(loc,b,CastCoerce) ->
-	  RCast(loc,replace_var_by_pattern b,CastCoerce)
-      | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+      | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GSort _ -> rt
+      | GHole _ -> rt
+      | GCast(loc,b,CastConv(k,t)) ->
+	  GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
+      | GCast(loc,b,CastCoerce) ->
+	  GCast(loc,replace_var_by_pattern b,CastCoerce)
+      | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
     if List.exists (fun id -> id_ord id x_id == 0) idl
     then br
@@ -590,21 +590,21 @@ let ids_of_rawterm c =
   let rec ids_of_rawterm acc c =
     let idof = id_of_name in
     match c with
-      | RVar (_,id) -> id::acc
-      | RApp (loc,g,args) ->
+      | GVar (_,id) -> id::acc
+      | GApp (loc,g,args) ->
           ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
-      | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
-      | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
-      | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
-      | RLetTuple (_,nal,(na,po),b,c) ->
+      | 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
+      | GLetTuple (_,nal,(na,po),b,c) ->
           List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCases (loc,sty,rtntypopt,tml,brchl) ->
+      | GCases (loc,sty,rtntypopt,tml,brchl) ->
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
-      | RRec _ -> failwith "Fix inside a constructor branch"
-      | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
+      | 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)
@@ -616,59 +616,59 @@ let ids_of_rawterm c =
 let zeta_normalize =
   let rec zeta_normalize_term rt =
     match rt with
-      | RRef _ -> rt
-      | RVar _ -> rt
-      | REvar _ -> rt
-      | RPatVar _ -> rt
-      | RApp(loc,rt',rtl) ->
-	  RApp(loc,
+      | GRef _ -> rt
+      | GVar _ -> rt
+      | GEvar _ -> rt
+      | GPatVar _ -> rt
+      | GApp(loc,rt',rtl) ->
+	  GApp(loc,
 	       zeta_normalize_term rt',
 	       List.map zeta_normalize_term rtl
 	      )
-      | RLambda(loc,name,k,t,b) ->
-	  RLambda(loc,
+      | GLambda(loc,name,k,t,b) ->
+	  GLambda(loc,
 		  name,
 		  k,
 		  zeta_normalize_term t,
 		  zeta_normalize_term b
 		 )
-      | RProd(loc,name,k,t,b) ->
-	  RProd(loc,
+      | GProd(loc,name,k,t,b) ->
+	  GProd(loc,
 		name,
 	        k,
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
-      | RLetIn(_,Name id,def,b) ->
+      | GLetIn(_,Name id,def,b) ->
 	  zeta_normalize_term (replace_var_by_term id def b)
-      | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
-      | RLetTuple(loc,nal,(na,rto),def,b) ->
-	  RLetTuple(loc,
+      | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
+      | GLetTuple(loc,nal,(na,rto),def,b) ->
+	  GLetTuple(loc,
 		    nal,
 		    (na,Option.map zeta_normalize_term rto),
 		    zeta_normalize_term def,
 		    zeta_normalize_term b
 		   )
-      | RCases(loc,sty,infos,el,brl) ->
-	  RCases(loc,sty,
+      | GCases(loc,sty,infos,el,brl) ->
+	  GCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
 		 List.map zeta_normalize_br brl
 		)
-      | RIf(loc,b,(na,e_option),lhs,rhs) ->
-	  RIf(loc, zeta_normalize_term b,
+      | GIf(loc,b,(na,e_option),lhs,rhs) ->
+	  GIf(loc, zeta_normalize_term b,
 	      (na,Option.map zeta_normalize_term e_option),
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
-      | RRec _ -> raise (UserError("",str "Not handled RRec"))
-      | RSort _ -> rt
-      | RHole _ -> rt
-      | RCast(loc,b,CastConv(k,t)) ->
-	  RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
-      | RCast(loc,b,CastCoerce) ->
-	  RCast(loc,zeta_normalize_term b,CastCoerce)
-      | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+      | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GSort _ -> rt
+      | GHole _ -> rt
+      | GCast(loc,b,CastConv(k,t)) ->
+	  GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
+      | GCast(loc,b,CastCoerce) ->
+	  GCast(loc,zeta_normalize_term b,CastCoerce)
+      | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and zeta_normalize_br (loc,idl,patl,res) =
     (loc,idl,patl,zeta_normalize_term res)
   in
@@ -688,29 +688,29 @@ let expand_as =
   in
   let rec expand_as map rt =
     match rt with
-      | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt
-      | RVar(_,id) ->
+      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt
+      | GVar(_,id) ->
 	  begin
 	    try
 	      Idmap.find id map
 	    with Not_found -> rt
 	  end
-      | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
-      | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
-      | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
-      | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
-      | RLetTuple(loc,nal,(na,po),v,b) ->
-	  RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
+      | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args)
+      | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b)
+      | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b)
+      | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b)
+      | GLetTuple(loc,nal,(na,po),v,b) ->
+	  GLetTuple(loc,nal,(na,Option.map (expand_as map) po),
 		    expand_as map v, expand_as map b)
-      | RIf(loc,e,(na,po),br1,br2) ->
-	  RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
+      | GIf(loc,e,(na,po),br1,br2) ->
+	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
-      | RRec _ ->  error "Not handled RRec"
-      | RDynamic _ -> error "Not handled RDynamic"
-      | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
-      | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
-      | RCases(loc,sty,po,el,brl) ->
-	  RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+      | GRec _ ->  error "Not handled GRec"
+      | GDynamic _ -> error "Not handled GDynamic"
+      | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t))
+      | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce)
+      | GCases(loc,sty,po,el,brl) ->
+	  GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
   and expand_as_br map (loc,idl,cpl,rt) =
     (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
index 465703386..9e872c236 100644
--- a/plugins/funind/rawtermops.mli
+++ b/plugins/funind/rawtermops.mli
@@ -7,60 +7,60 @@ val idmap_is_empty : 'a Names.Idmap.t -> bool
 (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
 val get_pattern_id : cases_pattern -> Names.identifier list
 
-(* [pattern_to_term pat] returns a rawconstr corresponding to [pat].
+(* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
    [pat] must not contain occurences of anonymous pattern
 *)
-val pattern_to_term : cases_pattern -> rawconstr
+val pattern_to_term : cases_pattern -> glob_constr
 
 (*
-   Some basic functions to rebuild rawconstr
+   Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-val mkRRef : Libnames.global_reference -> rawconstr
-val mkRVar : Names.identifier -> rawconstr
-val mkRApp  : rawconstr*(rawconstr list) -> rawconstr
-val mkRLambda : Names.name * rawconstr * rawconstr -> rawconstr
-val mkRProd : Names.name * rawconstr * rawconstr -> rawconstr
-val mkRLetIn : Names.name * rawconstr * rawconstr -> rawconstr
-val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr
-val mkRSort : rawsort -> rawconstr
-val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
-val mkRCast : rawconstr* rawconstr -> rawconstr
+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 : rawsort -> glob_constr
+val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
+val mkRCast : glob_constr* glob_constr -> glob_constr
 (*
-  Some basic functions to decompose rawconstrs
+  Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
-val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
-val raw_decompose_prod_or_letin :
-  rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr
-val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
-val raw_decompose_prod_or_letin_n : int -> rawconstr ->
-  (Names.name*rawconstr option*rawconstr option) list * rawconstr
-val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list  ->  rawconstr
-val raw_compose_prod_or_letin: rawconstr ->
-  (Names.name*rawconstr option*rawconstr option) list  ->  rawconstr
-val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
-
-
-(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-val  raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
-(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
-val  raw_make_neq : rawconstr -> rawconstr -> rawconstr
-(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
-val  raw_make_or : rawconstr -> rawconstr -> rawconstr
-
-(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
+val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr
+val glob_decompose_prod_or_letin :
+  glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr
+val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr
+val glob_decompose_prod_or_letin_n : int -> glob_constr ->
+  (Names.name*glob_constr option*glob_constr option) list * glob_constr
+val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list  ->  glob_constr
+val glob_compose_prod_or_letin: glob_constr ->
+  (Names.name*glob_constr option*glob_constr option) list  ->  glob_constr
+val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
+
+
+(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *)
+val  glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr
+(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
+val  glob_make_neq : glob_constr -> glob_constr -> glob_constr
+(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
+val  glob_make_or : glob_constr -> glob_constr -> glob_constr
+
+(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
    to [P1 \/ ( .... \/ Pn)]
 *)
-val  raw_make_or_list : rawconstr list -> rawconstr
+val  glob_make_or_list : glob_constr list -> glob_constr
 
 
 (* alpha_conversion functions *)
 
 
 
-(* Replace the var mapped in the rawconstr/context *)
-val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
+(* Replace the var mapped in the glob_constr/context *)
+val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
 
 
 
@@ -80,27 +80,27 @@ val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
 (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
    conventions and  does not share bound variables with avoid
 *)
-val alpha_rt : Names.identifier list -> rawconstr -> rawconstr
+val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
 val alpha_br : Names.identifier list ->
     Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.rawconstr ->
+    Rawterm.glob_constr ->
     Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.rawconstr
+    Rawterm.glob_constr
 
 
 (* Reduction function *)
 val replace_var_by_term  :
   Names.identifier ->
-  Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr
+  Rawterm.glob_constr -> Rawterm.glob_constr -> Rawterm.glob_constr
 
 
 
 (*
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
-val is_free_in : Names.identifier -> rawconstr -> bool
+val is_free_in : Names.identifier -> glob_constr -> bool
 
 
 val are_unifiable : cases_pattern -> cases_pattern -> bool
@@ -115,12 +115,12 @@ 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: rawconstr -> Names.Idset.t
+val ids_of_rawterm: glob_constr -> Names.Idset.t
 
 (*
    removing let_in construction in a rawterm
 *)
-val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
+val zeta_normalize : Rawterm.glob_constr -> Rawterm.glob_constr
 
 
-val expand_as : rawconstr -> rawconstr
+val expand_as : glob_constr -> glob_constr
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f066e39d0..1b43d4045 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1107,22 +1107,22 @@ let (value_f:constr list -> global_reference -> constr) =
       )
     in
     let fun_body =
-      RCases
+      GCases
 	(d0,RegularStyle,None,
-	 [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l),
+	 [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
 	  (Anonymous,None)],
 	 [d0, [v_id], [PatCstr(d0,(ind_of_ref
 				     (delayed_force coq_sig_ref),1),
 			       [PatVar(d0, Name v_id);
 				PatVar(d0, Anonymous)],
 			       Anonymous)],
-	  RVar(d0,v_id)])
+	  GVar(d0,v_id)])
     in
     let value =
       List.fold_left2
 	(fun acc x_id a ->
-	   RLambda
-      	     (d0, Name x_id, Explicit, RDynamic(d0, constr_in a),
+	   GLambda
+      	     (d0, Name x_id, Explicit, GDynamic(d0, constr_in a),
 	      acc
 	     )
 	)