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

10 files changed, 353 insertions, 353 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c61edbc55e..5115b3e3b7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -66,9 +66,9 @@ let error_needs_inversion env x t =
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
+    (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
     type_constraint ->
-    env -> rawconstr option * tomatch_tuples * cases_clauses ->
+    env -> glob_constr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
@@ -348,7 +348,7 @@ let find_tomatch_tycon evdref env loc = function
       empty_tycon,None
 
 let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
-  let loc = Some (loc_of_rawconstr tomatch) in
+  let loc = Some (loc_of_glob_constr tomatch) in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref tomatch in
   let typ = nf_evar !evdref j.uj_type in
@@ -1228,7 +1228,7 @@ let matx_of_eqns env tomatchl eqns =
     let initial_rhs = rhs in
     let rhs =
       { rhs_env = env;
-        rhs_vars = free_rawvars initial_rhs;
+        rhs_vars = free_glob_vars initial_rhs;
 	avoid_ids = ids@(ids_of_named_context (named_context env));
 	it = Some initial_rhs } in
     { patterns = initial_lpat;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 2facf8696f..015b386a55 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -61,9 +61,9 @@ type tomatch_status =
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
+    (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
     type_constraint ->
-    env -> rawconstr option * tomatch_tuples * cases_clauses ->
+    env -> glob_constr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 04dc132903..7469111bfc 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -275,30 +275,30 @@ let is_nondep_branch c n =
 let extract_nondep_branches test c b n =
   let rec strip n r = if n=0 then r else
     match r with
-      | RLambda (_,_,_,_,t) -> strip (n-1) t
-      | RLetIn (_,_,_,t) -> strip (n-1) t
+      | GLambda (_,_,_,_,t) -> strip (n-1) t
+      | GLetIn (_,_,_,t) -> strip (n-1) t
       | _ -> assert false in
   if test c n then Some (strip n b) else None
 
 let it_destRLambda_or_LetIn_names n c =
   let rec aux n nal c =
     if n=0 then (List.rev nal,c) else match c with
-      | RLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c
-      | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
+      | GLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c
+      | GLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
       | _ ->
           (* eta-expansion *)
 	  let rec next l =
 	    let x = next_ident_away (id_of_string "x") l in
-	    (* Not efficient but unusual and no function to get free rawvars *)
-(* 	    if occur_rawconstr x c then next (x::l) else x in *)
+	    (* Not efficient but unusual and no function to get free glob_vars *)
+(* 	    if occur_glob_constr x c then next (x::l) else x in *)
 	    x
 	  in
-	  let x = next (free_rawvars c) in
-	  let a = RVar (dl,x) in
+	  let x = next (free_glob_vars c) in
+	  let a = GVar (dl,x) in
 	  aux (n-1) (Name x :: nal)
             (match c with
-              | RApp (loc,p,l) -> RApp (loc,c,l@[a])
-              | _ -> (RApp (dl,c,[a])))
+              | GApp (loc,p,l) -> GApp (loc,c,l@[a])
+              | _ -> (GApp (dl,c,[a])))
   in aux n [] c
 
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
@@ -315,7 +315,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
         | Some p ->
             let nl,typ = it_destRLambda_or_LetIn_names k p in
 	    let n,typ = match typ with
-              | RLambda (_,x,_,t,c) -> x, c
+              | GLambda (_,x,_,t,c) -> x, c
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
@@ -341,20 +341,20 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   | LetStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
       let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
-      RLetTuple (dl,nal,(alias,pred),tomatch,d)
+      GLetTuple (dl,nal,(alias,pred),tomatch,d)
   | IfStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
       let nondepbrs =
 	array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
       if array_for_all ((<>) None) nondepbrs then
-	RIf (dl,tomatch,(alias,pred),
+	GIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
 	let eqnl = detype_eqns constructs consnargsl bl in
-	RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+	GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
       let eqnl = detype_eqns constructs consnargsl bl in
-      RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+      GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
   | Prop c -> RProp c
@@ -372,36 +372,36 @@ let rec detype (isgoal:bool) avoid env t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
-	 | Name id   -> RVar (dl, id)
+	 | Name id   -> GVar (dl, id)
 	 | Anonymous -> !detype_anonymous dl n
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
-	 in RVar (dl, id_of_string s))
+	 in GVar (dl, id_of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
-	REvar (dl, n, None)
+	GEvar (dl, n, None)
     | Var id ->
 	(try
-	  let _ = Global.lookup_named id in RRef (dl, VarRef id)
+	  let _ = Global.lookup_named id in GRef (dl, VarRef id)
 	 with _ ->
-	  RVar (dl, id))
-    | Sort s -> RSort (dl,detype_sort s)
+	  GVar (dl, id))
+    | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	RCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
+	GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
     | App (f,args) ->
-	RApp (dl,detype isgoal avoid env f,
+	GApp (dl,detype isgoal avoid env f,
               array_map_to_list (detype isgoal avoid env) args)
-    | Const sp -> RRef (dl, ConstRef sp)
+    | Const sp -> GRef (dl, ConstRef sp)
     | Evar (ev,cl) ->
-        REvar (dl, ev,
+        GEvar (dl, ev,
                Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
     | Ind ind_sp ->
-	RRef (dl, IndRef ind_sp)
+	GRef (dl, IndRef ind_sp)
     | Construct cstr_sp ->
-	RRef (dl, ConstructRef cstr_sp)
+	GRef (dl, ConstructRef cstr_sp)
     | Case (ci,p,c,bl) ->
 	let comp = computable p (ci.ci_pp_info.ind_nargs) in
 	detype_case comp (detype isgoal avoid env)
@@ -424,7 +424,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+  GRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -440,7 +440,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) =
   let v = array_map2
     (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t))
     bodies tys in
-  RRec(dl,RCoFix n,Array.of_list (List.rev lfi),
+  GRec(dl,RCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -535,9 +535,9 @@ and detype_binder isgoal bk avoid env na ty c =
     else compute_displayed_name_in flag avoid na c in
   let r =  detype isgoal avoid' (add_name na' env) c in
   match bk with
-  | BProd -> RProd (dl, na',Explicit,detype false avoid env ty, r)
-  | BLambda -> RLambda (dl, na',Explicit,detype false avoid env ty, r)
-  | BLetIn -> RLetIn (dl, na',detype false avoid env ty, r)
+  | BProd -> GProd (dl, na',Explicit,detype false avoid env ty, r)
+  | BLambda -> GLambda (dl, na',Explicit,detype false avoid env ty, r)
+  | BLetIn -> GLetIn (dl, na',detype false avoid env ty, r)
 
 let rec detype_rel_context where avoid env sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
@@ -569,42 +569,42 @@ let rec subst_cases_pattern subst pat =
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
 
-let rec subst_rawconstr subst raw =
+let rec subst_glob_constr subst raw =
   match raw with
-  | RRef (loc,ref) ->
+  | GRef (loc,ref) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
          detype false [] [] t
 
-  | RVar _ -> raw
-  | REvar _ -> raw
-  | RPatVar _ -> raw
+  | GVar _ -> raw
+  | GEvar _ -> raw
+  | GPatVar _ -> raw
 
-  | RApp (loc,r,rl) ->
-      let r' = subst_rawconstr subst r
-      and rl' = list_smartmap (subst_rawconstr subst) rl in
+  | GApp (loc,r,rl) ->
+      let r' = subst_glob_constr subst r
+      and rl' = list_smartmap (subst_glob_constr subst) rl in
 	if r' == r && rl' == rl then raw else
-	  RApp(loc,r',rl')
+	  GApp(loc,r',rl')
 
-  | RLambda (loc,n,bk,r1,r2) ->
-      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
+  | GLambda (loc,n,bk,r1,r2) ->
+      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  RLambda (loc,n,bk,r1',r2')
+	  GLambda (loc,n,bk,r1',r2')
 
-  | RProd (loc,n,bk,r1,r2) ->
-      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
+  | GProd (loc,n,bk,r1,r2) ->
+      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  RProd (loc,n,bk,r1',r2')
+	  GProd (loc,n,bk,r1',r2')
 
-  | RLetIn (loc,n,r1,r2) ->
-      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
+  | GLetIn (loc,n,r1,r2) ->
+      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  RLetIn (loc,n,r1',r2')
+	  GLetIn (loc,n,r1',r2')
 
-  | RCases (loc,sty,rtno,rl,branches) ->
-      let rtno' = Option.smartmap (subst_rawconstr subst) rtno
+  | GCases (loc,sty,rtno,rl,branches) ->
+      let rtno' = Option.smartmap (subst_glob_constr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
-        let a' = subst_rawconstr subst a in
+        let a' = subst_glob_constr subst a in
         let (n,topt) = x in
         let topt' = Option.smartmap
           (fun (loc,(sp,i),x,y as t) ->
@@ -615,61 +615,61 @@ let rec subst_rawconstr subst raw =
 			(fun (loc,idl,cpl,r as branch) ->
 			   let cpl' =
 			     list_smartmap (subst_cases_pattern subst) cpl
-			   and r' = subst_rawconstr subst r in
+			   and r' = subst_glob_constr subst r in
 			     if cpl' == cpl && r' == r then branch else
 			       (loc,idl,cpl',r'))
 			branches
       in
 	if rtno' == rtno && rl' == rl && branches' == branches then raw else
-	  RCases (loc,sty,rtno',rl',branches')
+	  GCases (loc,sty,rtno',rl',branches')
 
-  | RLetTuple (loc,nal,(na,po),b,c) ->
-      let po' = Option.smartmap (subst_rawconstr subst) po
-      and b' = subst_rawconstr subst b
-      and c' = subst_rawconstr subst c in
+  | GLetTuple (loc,nal,(na,po),b,c) ->
+      let po' = Option.smartmap (subst_glob_constr subst) po
+      and b' = subst_glob_constr subst b
+      and c' = subst_glob_constr subst c in
 	if po' == po && b' == b && c' == c then raw else
-          RLetTuple (loc,nal,(na,po'),b',c')
+          GLetTuple (loc,nal,(na,po'),b',c')
 
-  | RIf (loc,c,(na,po),b1,b2) ->
-      let po' = Option.smartmap (subst_rawconstr subst) po
-      and b1' = subst_rawconstr subst b1
-      and b2' = subst_rawconstr subst b2
-      and c' = subst_rawconstr subst c in
+  | GIf (loc,c,(na,po),b1,b2) ->
+      let po' = Option.smartmap (subst_glob_constr subst) po
+      and b1' = subst_glob_constr subst b1
+      and b2' = subst_glob_constr subst b2
+      and c' = subst_glob_constr subst c in
 	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
-          RIf (loc,c',(na,po'),b1',b2')
+          GIf (loc,c',(na,po'),b1',b2')
 
-  | RRec (loc,fix,ida,bl,ra1,ra2) ->
-      let ra1' = array_smartmap (subst_rawconstr subst) ra1
-      and ra2' = array_smartmap (subst_rawconstr subst) ra2 in
+  | GRec (loc,fix,ida,bl,ra1,ra2) ->
+      let ra1' = array_smartmap (subst_glob_constr subst) ra1
+      and ra2' = array_smartmap (subst_glob_constr subst) ra2 in
       let bl' = array_smartmap
         (list_smartmap (fun (na,k,obd,ty as dcl) ->
-          let ty' = subst_rawconstr subst ty in
-          let obd' = Option.smartmap (subst_rawconstr subst) obd in
+          let ty' = subst_glob_constr subst ty in
+          let obd' = Option.smartmap (subst_glob_constr subst) obd in
           if ty'==ty & obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
-	  RRec (loc,fix,ida,bl',ra1',ra2')
+	  GRec (loc,fix,ida,bl',ra1',ra2')
 
-  | RSort _ -> raw
+  | GSort _ -> raw
 
-  | RHole (loc,ImplicitArg (ref,i,b)) ->
+  | GHole (loc,ImplicitArg (ref,i,b)) ->
       let ref',_ = subst_global subst ref in
 	if ref' == ref then raw else
-	  RHole (loc,InternalHole)
-  | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
+	  GHole (loc,InternalHole)
+  | GHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
       TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) ->
       raw
 
-  | RCast (loc,r1,k) ->
+  | GCast (loc,r1,k) ->
       (match k with
 	   CastConv (k,r2) ->
-	     let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
+	     let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	       if r1' == r1 && r2' == r2 then raw else
-		 RCast (loc,r1', CastConv (k,r2'))
+		 GCast (loc,r1', CastConv (k,r2'))
 	 | CastCoerce ->
-	     let r1' = subst_rawconstr subst r1 in
-	       if r1' == r1 then raw else RCast (loc,r1',k))
-  | RDynamic _ -> raw
+	     let r1' = subst_glob_constr subst r1 in
+	       if r1' == r1 then raw else GCast (loc,r1',k))
+  | GDynamic _ -> raw
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index e178a4ca3f..e2644592cb 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -17,40 +17,40 @@ open Mod_subst
 
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
-val subst_rawconstr : substitution -> rawconstr -> rawconstr
+val subst_glob_constr : substitution -> glob_constr -> glob_constr
 
-(** [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr 
+(** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr 
    de Bruijn indexes are turned to bound names, avoiding names in [avoid] 
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
    [ctx] gives the names of the free variables *)
 
-val detype : bool -> identifier list -> names_context -> constr -> rawconstr
+val detype : bool -> identifier list -> names_context -> constr -> glob_constr
 
 val detype_case :
-  bool -> ('a -> rawconstr) ->
+  bool -> ('a -> glob_constr) ->
   (constructor array -> int array -> 'a array ->
-    (loc * identifier list * cases_pattern list * rawconstr) list) ->
+    (loc * identifier list * cases_pattern list * glob_constr) list) ->
   ('a -> int -> bool) ->
   identifier list -> inductive * case_style * int * int array * int ->
-    'a option -> 'a -> 'a array -> rawconstr
+    'a option -> 'a -> 'a array -> glob_constr
 
 val detype_sort : sorts -> rawsort
 
 val detype_rel_context : constr option -> identifier list -> names_context ->
-  rel_context -> rawdecl list
+  rel_context -> glob_decl list
 
 (** look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_displayed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
 
-val set_detype_anonymous : (loc -> int -> rawconstr) -> unit
+val set_detype_anonymous : (loc -> int -> glob_constr) -> unit
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
 (** Utilities to transform kernel cases to simple pattern-matching problem *)
 
-val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
+val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_constr
 val simple_cases_matrix_of_branches :
-  inductive -> int list -> rawconstr list -> cases_clauses
+  inductive -> int list -> glob_constr list -> cases_clauses
 val return_type_of_predicate :
-  inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option
+  inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr option
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 15bc06e025..2217074fe4 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -248,48 +248,48 @@ let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
 let rec pat_of_raw metas vars = function
-  | RVar (_,id) ->
+  | GVar (_,id) ->
       (try PRel (list_index (Name id) vars)
        with Not_found -> PVar id)
-  | RPatVar (_,(false,n)) ->
+  | GPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
-  | RRef (_,gr) ->
+  | GRef (_,gr) ->
       PRef (canonical_gr gr)
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
-  | RApp (_, RPatVar (_,(true,n)), cl) ->
+  | GApp (_, GPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | RApp (_,c,cl) ->
+  | GApp (_,c,cl) ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-  | RLambda (_,na,bk,c1,c2) ->
+  | GLambda (_,na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RProd (_,na,bk,c1,c2) ->
+  | GProd (_,na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RLetIn (_,na,c1,c2) ->
+  | GLetIn (_,na,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RSort (_,s) ->
+  | GSort (_,s) ->
       PSort s
-  | RHole _ ->
+  | GHole _ ->
       PMeta None
-  | RCast (_,c,_) ->
+  | GCast (_,c,_) ->
       Flags.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
-  | RIf (_,c,(_,None),b1,b2) ->
+  | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
-  | RLetTuple (loc,nal,(_,None),b,c) ->
-      let mkRLambda c na = RLambda (loc,na,Explicit,RHole (loc,Evd.InternalHole),c) in
+  | 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
       PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
              [|pat_of_raw metas vars c|])
-  | RCases (loc,sty,p,[c,(na,indnames)],brs) ->
+  | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
       let pred,ind_nargs, ind = match p,indnames with
 	| Some p, Some (_,ind,n,nal) ->
 	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
@@ -307,34 +307,34 @@ let rec pat_of_raw metas vars = function
              pat_of_raw metas vars c, brs)
 
   | r ->
-      let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.")
+      let loc = loc_of_glob_constr r in
+      user_err_loc (loc,"pattern_of_glob_constr", Pp.str"Non supported pattern.")
 
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
     (function
         (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
       | (loc,_,_,_) ->
-          user_err_loc (loc,"pattern_of_rawconstr",
+          user_err_loc (loc,"pattern_of_glob_constr",
                         Pp.str "Non supported pattern.")) brs in
   match bri with
     | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
 	if ind <> None & ind <> Some indsp then
-          user_err_loc (loc,"pattern_of_rawconstr",
+          user_err_loc (loc,"pattern_of_glob_constr",
             Pp.str "All constructors must be in the same inductive type.");
         let lna =
           List.map
             (function PatVar(_,na) -> na
               | PatCstr(loc,_,_,_) ->
-                  user_err_loc (loc,"pattern_of_rawconstr",
+                  user_err_loc (loc,"pattern_of_glob_constr",
                                 Pp.str "Non supported pattern.")) lv in
         let vars' = List.rev lna @ vars in
 	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
-    | _ -> user_err_loc (loc,"pattern_of_rawconstr",
+    | _ -> user_err_loc (loc,"pattern_of_glob_constr",
                          str "No unique branch for " ++ int (i+1) ++
                          str"-th constructor.")
 
-let pattern_of_rawconstr c =
+let pattern_of_glob_constr c =
   let metas = ref [] in
   let p = pat_of_raw metas [] c in	
   (!metas,p)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 7dadb78f30..a739a28887 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -103,11 +103,11 @@ val head_of_constr_reference : Term.constr -> global_reference
 
 val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
 
-(** [pattern_of_rawconstr l c] translates a term [c] with metavariables into
+(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
     are bound *)
 
-val pattern_of_rawconstr : rawconstr ->
+val pattern_of_glob_constr : glob_constr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7017edaf28..bc80296d57 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -48,7 +48,7 @@ type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
-type rawconstr_ltac_closure = ltac_var_map * rawconstr
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -86,7 +86,7 @@ let search_guard loc env possible_indexes fixdefs =
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
      with Found indexes -> indexes)
 
-(* To embed constr in rawconstr *)
+(* To embed constr in glob_constr *)
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
@@ -109,19 +109,19 @@ sig
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   val allow_anonymous_refs : bool ref
 
-  (* Generic call to the interpreter from rawconstr to open_constr, leaving
+  (* Generic call to the interpreter from glob_constr to open_constr, leaving
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
 
   val understand_tcc : ?resolve_classes:bool ->
-    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+    evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
 
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_map ref -> env -> typing_constraint -> rawconstr -> constr
+    evar_map ref -> env -> typing_constraint -> glob_constr -> constr
 
   (* More general entry point with evars from ltac *)
 
-  (* Generic call to the interpreter from rawconstr to constr, failing
+  (* Generic call to the interpreter from glob_constr to constr, failing
      unresolved holes in the rawterm cannot be instantiated.
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
@@ -134,29 +134,29 @@ sig
 
   val understand_ltac :
     bool -> evar_map -> env -> ltac_var_map ->
-    typing_constraint -> rawconstr -> evar_map * constr
+    typing_constraint -> glob_constr -> evar_map * constr
 
-  (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+  (* Standard call to get a constr from a glob_constr, resolving implicit args *)
 
   val understand : evar_map -> env -> ?expected_type:Term.types ->
-    rawconstr -> constr
+    glob_constr -> constr
 
-  (* Idem but the rawconstr is intended to be a type *)
+  (* Idem but the glob_constr is intended to be a type *)
 
-  val understand_type : evar_map -> env -> rawconstr -> constr
+  val understand_type : evar_map -> env -> glob_constr -> constr
 
   (* A generalization of the two previous case *)
 
   val understand_gen : typing_constraint -> evar_map -> env ->
-    rawconstr -> constr
+    glob_constr -> constr
 
   (* Idem but returns the judgment of the understood term *)
 
-  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
 
   (* Idem but do not fail on unresolved evars *)
 
-  val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
 
   (*i*)
   (* Internal of Pretyping...
@@ -164,15 +164,15 @@ sig
    *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_judgment
+    ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_type_judgment
+    ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    ltac_var_map -> typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> glob_constr -> constr
 
     (*i*)
 end
@@ -302,17 +302,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* in environment [env], with existential variables [evdref] and *)
   (* the type constraint tycon *)
   let rec pretype (tycon : type_constraint) env evdref lvar = function
-    | RRef (loc,ref) ->
+    | GRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_ref evdref env ref)
 	  tycon
 
-    | RVar (loc, id) ->
+    | GVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
-    | REvar (loc, evk, instopt) ->
+    | GEvar (loc, evk, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
 	let hyps = evar_filtered_context (Evd.find !evdref evk) in
@@ -323,7 +323,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j = (Retyping.get_judgment_of env !evdref c) in
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
-    | RPatVar (loc,(someta,n)) ->
+    | GPatVar (loc,(someta,n)) ->
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
@@ -332,7 +332,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
         let k = MatchingVar (someta,n) in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | RHole (loc,k) ->
+    | GHole (loc,k) ->
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
@@ -340,7 +340,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | RRec (loc,fixkind,names,bl,lar,vdef) ->
+    | GRec (loc,fixkind,names,bl,lar,vdef) ->
 	let rec type_bl env ctxt = function
             [] -> ctxt
           | (na,bk,None,ty)::bl ->
@@ -403,16 +403,16 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
-    | RSort (loc,s) ->
+    | GSort (loc,s) ->
 	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
 
-    | RApp (loc,f,args) ->
+    | GApp (loc,f,args) ->
 	let fj = pretype empty_tycon env evdref lvar f in
- 	let floc = loc_of_rawconstr f in
+ 	let floc = loc_of_glob_constr f in
 	let rec apply_rec env n resj = function
 	  | [] -> resj
 	  | c::rest ->
-	      let argloc = loc_of_rawconstr c in
+	      let argloc = loc_of_glob_constr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
               let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
@@ -446,7 +446,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLambda(loc,name,bk,c1,c2)      ->
+    | GLambda(loc,name,bk,c1,c2)      ->
 	let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env evdref lvar c1 in
@@ -454,7 +454,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j' = pretype rng (push_rel var env) evdref lvar c2 in
 	  judge_of_abstraction env (orelse_name name name') j j'
 
-    | RProd(loc,name,bk,c1,c2)        ->
+    | GProd(loc,name,bk,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let j' =
 	  if name = Anonymous then
@@ -470,10 +470,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  with TypeError _ as e -> Loc.raise loc e in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLetIn(loc,name,c1,c2)      ->
+    | GLetIn(loc,name,c1,c2)      ->
 	let j =
 	  match c1 with
-	  | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	  | GCast (loc, c, CastConv (DEFAULTcast, t)) ->
 	      let tj = pretype_type empty_valcon env evdref lvar t in
 		pretype (mk_tycon tj.utj_val) env evdref lvar c
 	  | _ -> pretype empty_tycon env evdref lvar c1
@@ -485,12 +485,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	    uj_type = subst1 j.uj_val j'.uj_type }
 
-    | RLetTuple (loc,nal,(na,po),c,d) ->
+    | GLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
 	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
+	    let cloc = loc_of_glob_constr c in
 	      error_case_not_inductive_loc cloc env !evdref cj
 	in
 	let cstrs = get_constructors env indf in
@@ -551,12 +551,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     in
 		       { uj_val = v; uj_type = ccl })
 
-    | RIf (loc,c,(na,po),b1,b2) ->
+    | GIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
 	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
+	    let cloc = loc_of_glob_constr c in
 	      error_case_not_inductive_loc cloc env !evdref cj in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 2 then
@@ -619,12 +619,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
-    | RCases (loc,sty,po,tml,eqns) ->
+    | GCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast (loc,c,k) ->
+    | GCast (loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
@@ -643,7 +643,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  { uj_val = v; uj_type = tval }
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | RDynamic (loc,d) ->
+    | GDynamic (loc,d) ->
 	if (Dyn.tag d) = "constr" then
 	  let c = constr_out d in
 	  let j = (Retyping.get_judgment_of env !evdref c) in
@@ -654,7 +654,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
-    | RHole loc ->
+    | GHole loc ->
 	(match valcon with
 	   | Some v ->
                let s =
@@ -674,7 +674,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   utj_type = s})
     | c ->
 	let j = pretype empty_tycon env evdref lvar c in
-	let loc = loc_of_rawconstr c in
+	let loc = loc_of_glob_constr c in
 	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	  match valcon with
 	    | None -> tj
@@ -682,7 +682,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env evdref v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env !evdref tj.utj_val v
+                    (loc_of_glob_constr c) env !evdref tj.utj_val v
 
   let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7f707de3d2..8c02707436 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This file implements type inference. It maps [rawconstr]
+(** This file implements type inference. It maps [glob_constr]
    (i.e. untyped terms whose names are located) to [constr]. In
    particular, it drives complex pattern-matching problems ("match")
    into elementary ones, insertion of coercions and resolution of
@@ -30,7 +30,7 @@ type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * Pattern.constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
-type rawconstr_ltac_closure = ltac_var_map * rawconstr
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
 
 module type S =
 sig
@@ -40,19 +40,19 @@ sig
   (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   val allow_anonymous_refs : bool ref
 
-  (** Generic call to the interpreter from rawconstr to open_constr, leaving
+  (** Generic call to the interpreter from glob_constr to open_constr, leaving
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
 
   val understand_tcc : ?resolve_classes:bool ->
-    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+    evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
 
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_map ref -> env -> typing_constraint -> rawconstr -> constr
+    evar_map ref -> env -> typing_constraint -> glob_constr -> constr
 
   (** More general entry point with evars from ltac *)
 
-  (** Generic call to the interpreter from rawconstr to constr, failing
+  (** Generic call to the interpreter from glob_constr to constr, failing
      unresolved holes in the rawterm cannot be instantiated.
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
@@ -65,42 +65,42 @@ sig
 
   val understand_ltac :
     bool -> evar_map -> env -> ltac_var_map ->
-    typing_constraint -> rawconstr -> evar_map * constr
+    typing_constraint -> glob_constr -> evar_map * constr
 
-  (** Standard call to get a constr from a rawconstr, resolving implicit args *)
+  (** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
   val understand : evar_map -> env -> ?expected_type:Term.types ->
-    rawconstr -> constr
+    glob_constr -> constr
 
-  (** Idem but the rawconstr is intended to be a type *)
+  (** Idem but the glob_constr is intended to be a type *)
 
-  val understand_type : evar_map -> env -> rawconstr -> constr
+  val understand_type : evar_map -> env -> glob_constr -> constr
 
   (** A generalization of the two previous case *)
 
   val understand_gen : typing_constraint -> evar_map -> env ->
-    rawconstr -> constr
+    glob_constr -> constr
 
   (** Idem but returns the judgment of the understood term *)
 
-  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
 
   (** Idem but do not fail on unresolved evars *)
-  val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
 
   (**/**)
   (** Internal of Pretyping... *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_judgment
+    ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_type_judgment
+    ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    ltac_var_map -> typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> glob_constr -> constr
 
   (**/**)
 
@@ -109,7 +109,7 @@ end
 module Pretyping_F (C : Coercion.S) : S
 module Default : S
 
-(** To embed constr in rawconstr *)
+(** To embed constr in glob_constr *)
 
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 88dc5db42f..deba9a257a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -49,29 +49,29 @@ type 'a cast_type =
   | CastConv of cast_kind * 'a
   | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
 
-type rawconstr =
-  | RRef of (loc * global_reference)
-  | RVar of (loc * identifier)
-  | REvar of loc * existential_key * rawconstr list option
-  | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
-  | RApp of loc * rawconstr * rawconstr list
-  | RLambda of loc * name * binding_kind * rawconstr * rawconstr
-  | RProd of loc * name * binding_kind * rawconstr * rawconstr
-  | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
-  | RLetTuple of loc * name list * (name * rawconstr option) *
-      rawconstr * rawconstr
-  | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
-  | RRec of loc * fix_kind * identifier array * rawdecl list array *
-      rawconstr array * rawconstr array
-  | RSort of loc * rawsort
-  | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * rawconstr cast_type
-  | RDynamic of loc * Dyn.t
-
-and rawdecl = name * binding_kind * rawconstr option * rawconstr
-
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
+type glob_constr =
+  | GRef of (loc * global_reference)
+  | GVar of (loc * identifier)
+  | GEvar of loc * existential_key * glob_constr list option
+  | GPatVar of loc * (bool * patvar) (* Used for patterns only *)
+  | GApp of loc * glob_constr * glob_constr list
+  | GLambda of loc * name * binding_kind * glob_constr * glob_constr
+  | GProd of loc * name * binding_kind * glob_constr * glob_constr
+  | GLetIn of loc * name * glob_constr * glob_constr
+  | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
+  | GLetTuple of loc * name list * (name * glob_constr option) *
+      glob_constr * glob_constr
+  | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
+  | GRec of loc * fix_kind * identifier array * glob_decl list array *
+      glob_constr array * glob_constr array
+  | GSort of loc * rawsort
+  | GHole of (loc * hole_kind)
+  | GCast of loc * glob_constr * glob_constr cast_type
+  | GDynamic of loc * Dyn.t
+
+and glob_decl = name * binding_kind * glob_constr option * glob_constr
+
+and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
@@ -80,11 +80,11 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern)
+and tomatch_tuple = (glob_constr * predicate_pattern)
 
 and tomatch_tuples = tomatch_tuple list
 
-and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
+and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
 
 and cases_clauses = cases_clause list
 
@@ -93,55 +93,55 @@ let cases_predicate_names tml =
     | (tm,(na,None)) -> [na]
     | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
 
-let map_rawdecl_left_to_right f (na,k,obd,ty) = 
+let map_glob_decl_left_to_right f (na,k,obd,ty) = 
   let comp1 = Option.map f obd in
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
-let map_rawconstr_left_to_right f = function
-  | RApp (loc,g,args) -> 
+let map_glob_constr_left_to_right f = function
+  | GApp (loc,g,args) -> 
       let comp1 = f g in 
       let comp2 = Util.list_map_left f args in 
-      RApp (loc,comp1,comp2)
-  | RLambda (loc,na,bk,ty,c) -> 
+      GApp (loc,comp1,comp2)
+  | GLambda (loc,na,bk,ty,c) -> 
       let comp1 = f ty in 
       let comp2 = f c in 
-      RLambda (loc,na,bk,comp1,comp2)
-  | RProd (loc,na,bk,ty,c) -> 
+      GLambda (loc,na,bk,comp1,comp2)
+  | GProd (loc,na,bk,ty,c) -> 
       let comp1 = f ty in 
       let comp2 = f c in 
-      RProd (loc,na,bk,comp1,comp2)
-  | RLetIn (loc,na,b,c) -> 
+      GProd (loc,na,bk,comp1,comp2)
+  | GLetIn (loc,na,b,c) -> 
       let comp1 = f b in 
       let comp2 = f c in 
-      RLetIn (loc,na,comp1,comp2)
-  | RCases (loc,sty,rtntypopt,tml,pl) ->
+      GLetIn (loc,na,comp1,comp2)
+  | GCases (loc,sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in 
       let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
       let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
-      RCases (loc,sty,comp1,comp2,comp3)
-  | RLetTuple (loc,nal,(na,po),b,c) ->
+      GCases (loc,sty,comp1,comp2,comp3)
+  | GLetTuple (loc,nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
       let comp2 = f b in
       let comp3 = f c in 
-      RLetTuple (loc,nal,(na,comp1),comp2,comp3)
-  | RIf (loc,c,(na,po),b1,b2) ->
+      GLetTuple (loc,nal,(na,comp1),comp2,comp3)
+  | GIf (loc,c,(na,po),b1,b2) ->
       let comp1 = Option.map f po in
       let comp2 = f b1 in
       let comp3 = f b2 in
-      RIf (loc,f c,(na,comp1),comp2,comp3)
-  | RRec (loc,fk,idl,bl,tyl,bv) ->
-      let comp1 = Array.map (Util.list_map_left (map_rawdecl_left_to_right f)) bl in
+      GIf (loc,f c,(na,comp1),comp2,comp3)
+  | GRec (loc,fk,idl,bl,tyl,bv) ->
+      let comp1 = Array.map (Util.list_map_left (map_glob_decl_left_to_right f)) bl in
       let comp2 = Array.map f tyl in
       let comp3 = Array.map f bv in
-      RRec (loc,fk,idl,comp1,comp2,comp3)
-  | RCast (loc,c,k) -> 
+      GRec (loc,fk,idl,comp1,comp2,comp3)
+  | GCast (loc,c,k) -> 
       let comp1 = f c in
       let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in
-      RCast (loc,comp1,comp2)
-  | (RVar _ | RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
+      GCast (loc,comp1,comp2)
+  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) as x -> x
 
-let map_rawconstr = map_rawconstr_left_to_right
+let map_glob_constr = map_glob_constr_left_to_right
 
 (*
 let name_app f e = function
@@ -154,54 +154,54 @@ let fold_ident g idl e =
       (fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e)
   in (Array.of_list idl,e)
 
-let map_rawconstr_with_binders_loc loc g f e = function
-  | RVar (_,id) -> RVar (loc,id)
-  | RApp (_,a,args) -> RApp (loc,f e a, List.map (f e) args)
-  | RLambda (_,na,ty,c) ->
-      let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
-  | RProd (_,na,ty,c) ->
-      let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
-  | RLetIn (_,na,b,c) ->
-      let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
-  | RCases (_,tyopt,tml,pl) ->
+let map_glob_constr_with_binders_loc loc g f e = function
+  | GVar (_,id) -> GVar (loc,id)
+  | GApp (_,a,args) -> GApp (loc,f e a, List.map (f e) args)
+  | GLambda (_,na,ty,c) ->
+      let na,e = name_app g e na in GLambda (loc,na,f e ty,f e c)
+  | GProd (_,na,ty,c) ->
+      let na,e = name_app g e na in GProd (loc,na,f e ty,f e c)
+  | GLetIn (_,na,b,c) ->
+      let na,e = name_app g e na in GLetIn (loc,na,f e b,f e c)
+  | GCases (_,tyopt,tml,pl) ->
       (* We don't modify pattern variable since we don't traverse patterns *)
       let g' id e = snd (g id e) in
       let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
-      RCases
+      GCases
 	(loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl)
-  | RRec (_,fk,idl,tyl,bv) ->
+  | GRec (_,fk,idl,tyl,bv) ->
       let idl',e' = fold_ident g idl e in
-      RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
-  | RCast (_,c,t) -> RCast (loc,f e c,f e t)
-  | RSort (_,x) -> RSort (loc,x)
-  | RHole (_,x)  -> RHole (loc,x)
-  | RRef (_,x) -> RRef (loc,x)
-  | REvar (_,x,l) -> REvar (loc,x,l)
-  | RPatVar (_,x) -> RPatVar (loc,x)
-  | RDynamic (_,x) -> RDynamic (loc,x)
+      GRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
+  | GCast (_,c,t) -> GCast (loc,f e c,f e t)
+  | GSort (_,x) -> GSort (loc,x)
+  | GHole (_,x)  -> GHole (loc,x)
+  | GRef (_,x) -> GRef (loc,x)
+  | GEvar (_,x,l) -> GEvar (loc,x,l)
+  | GPatVar (_,x) -> GPatVar (loc,x)
+  | GDynamic (_,x) -> GDynamic (loc,x)
 *)
 
-let fold_rawconstr f acc =
+let fold_glob_constr f acc =
   let rec fold acc = function
-  | RVar _ -> acc
-  | RApp (_,c,args) -> List.fold_left fold (fold acc c) args
-  | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) ->
+  | GVar _ -> acc
+  | GApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) ->
       fold (fold acc b) c
-  | RCases (_,_,rtntypopt,tml,pl) ->
+  | GCases (_,_,rtntypopt,tml,pl) ->
       List.fold_left fold_pattern
 	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
 	pl
-    | RLetTuple (_,_,rtntyp,b,c) ->
+    | GLetTuple (_,_,rtntyp,b,c) ->
 	fold (fold (fold_return_type acc rtntyp) b) c
-    | RIf (_,c,rtntyp,b1,b2) ->
+    | GIf (_,c,rtntyp,b1,b2) ->
 	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
-    | RRec (_,_,_,bl,tyl,bv) ->
+    | GRec (_,_,_,bl,tyl,bv) ->
 	let acc = Array.fold_left
 	  (List.fold_left (fun acc (na,k,bbd,bty) ->
 	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
 	Array.fold_left fold (Array.fold_left fold acc tyl) bv
-    | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
-    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc
+    | GCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> acc
 
   and fold_pattern acc (_,idl,p,c) = fold acc c
 
@@ -209,25 +209,25 @@ let fold_rawconstr f acc =
 
   in fold acc
 
-let iter_rawconstr f = fold_rawconstr (fun () -> f) ()
+let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
-let occur_rawconstr id =
+let occur_glob_constr id =
   let rec occur = function
-    | RVar (loc,id') -> id = id'
-    | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
-    | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
-    | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
-    | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RCases (loc,sty,rtntypopt,tml,pl) ->
+    | GVar (loc,id') -> id = id'
+    | GApp (loc,f,args) -> (occur f) or (List.exists occur args)
+    | GLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | GProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | GLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
+    | GCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
 	or (List.exists occur_pattern pl)
-    | RLetTuple (loc,nal,rtntyp,b,c) ->
+    | GLetTuple (loc,nal,rtntyp,b,c) ->
 	occur_return_type rtntyp id
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
-    | RIf (loc,c,rtntyp,b1,b2) ->
+    | GIf (loc,c,rtntyp,b1,b2) ->
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
-    | RRec (loc,fk,idl,bl,tyl,bv) ->
+    | GRec (loc,fk,idl,bl,tyl,bv) ->
         not (array_for_all4 (fun fid bl ty bd ->
           let rec occur_fix = function
               [] -> not (occur ty) && (fid=id or not(occur bd))
@@ -239,8 +239,8 @@ let occur_rawconstr id =
                 (na=Name id or not(occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
-    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
+    | GCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
 
@@ -256,29 +256,29 @@ let add_name_to_ids set na =
     | Anonymous -> set
     | Name id -> Idset.add id set
 
-let free_rawvars  =
+let free_glob_vars  =
   let rec vars bounded vs = function
-    | RVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
-    | RApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
+    | GVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
+    | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
+    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
 	let vs' = vars bounded vs ty in
 	let bounded' = add_name_to_ids bounded na in
        vars bounded' vs' c
-    | RCases (loc,sty,rtntypopt,tml,pl) ->
+    | GCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
 	List.fold_left (vars_pattern bounded) vs2 pl
-    | RLetTuple (loc,nal,rtntyp,b,c) ->
+    | GLetTuple (loc,nal,rtntyp,b,c) ->
 	let vs1 = vars_return_type bounded vs rtntyp in
 	let vs2 = vars bounded vs1 b in
 	let bounded' = List.fold_left add_name_to_ids bounded nal in
 	vars bounded' vs2 c
-    | RIf (loc,c,rtntyp,b1,b2) ->
+    | GIf (loc,c,rtntyp,b1,b2) ->
 	let vs1 = vars_return_type bounded vs rtntyp in
 	let vs2 = vars bounded vs1 c in
 	let vs3 = vars bounded vs2 b1 in
 	vars bounded vs3 b2
-    | RRec (loc,fk,idl,bl,tyl,bv) ->
+    | GRec (loc,fk,idl,bl,tyl,bv) ->
 	let bounded' = Array.fold_right Idset.add idl bounded in
 	let vars_fix i vs fid =
 	  let vs1,bounded1 =
@@ -296,9 +296,9 @@ let free_rawvars  =
 	  vars bounded1 vs2 bv.(i)
 	in
 	array_fold_left_i vars_fix vs idl
-    | RCast (loc,c,k) -> let v = vars bounded vs c in
+    | GCast (loc,c,k) -> let v = vars bounded vs c in
 	(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
-    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) =
     let bounded' = List.fold_right Idset.add idl bounded  in
@@ -315,51 +315,51 @@ let free_rawvars  =
     Idset.elements vs
 
 
-let loc_of_rawconstr = function
-  | RRef (loc,_) -> loc
-  | RVar (loc,_) -> loc
-  | REvar (loc,_,_) -> loc
-  | RPatVar (loc,_) -> loc
-  | RApp (loc,_,_) -> loc
-  | RLambda (loc,_,_,_,_) -> loc
-  | RProd (loc,_,_,_,_) -> loc
-  | RLetIn (loc,_,_,_) -> loc
-  | RCases (loc,_,_,_,_) -> loc
-  | RLetTuple (loc,_,_,_,_) -> loc
-  | RIf (loc,_,_,_,_) -> loc
-  | RRec (loc,_,_,_,_,_) -> loc
-  | RSort (loc,_) -> loc
-  | RHole (loc,_) -> loc
-  | RCast (loc,_,_) -> loc
-  | RDynamic (loc,_) -> loc
+let loc_of_glob_constr = function
+  | GRef (loc,_) -> loc
+  | GVar (loc,_) -> loc
+  | GEvar (loc,_,_) -> loc
+  | GPatVar (loc,_) -> loc
+  | GApp (loc,_,_) -> loc
+  | GLambda (loc,_,_,_,_) -> loc
+  | GProd (loc,_,_,_,_) -> loc
+  | GLetIn (loc,_,_,_) -> loc
+  | GCases (loc,_,_,_,_) -> loc
+  | GLetTuple (loc,_,_,_,_) -> loc
+  | GIf (loc,_,_,_,_) -> loc
+  | GRec (loc,_,_,_,_,_) -> loc
+  | GSort (loc,_) -> loc
+  | GHole (loc,_) -> loc
+  | GCast (loc,_,_) -> loc
+  | GDynamic (loc,_) -> loc
 
 (**********************************************************************)
-(* Conversion from rawconstr to cases pattern, if possible            *)
+(* Conversion from glob_constr to cases pattern, if possible            *)
 
-let rec cases_pattern_of_rawconstr na = function
-  | RVar (loc,id) when na<>Anonymous ->
+let rec cases_pattern_of_glob_constr na = function
+  | GVar (loc,id) when na<>Anonymous ->
       (* Unable to manage the presence of both an alias and a variable *)
       raise Not_found
-  | RVar (loc,id) -> PatVar (loc,Name id)
-  | RHole (loc,_) -> PatVar (loc,na)
-  | RRef (loc,ConstructRef cstr) ->
+  | GVar (loc,id) -> PatVar (loc,Name id)
+  | GHole (loc,_) -> PatVar (loc,na)
+  | GRef (loc,ConstructRef cstr) ->
       PatCstr (loc,cstr,[],na)
-  | RApp (loc,RRef (_,ConstructRef cstr),l) ->
-      PatCstr (loc,cstr,List.map (cases_pattern_of_rawconstr Anonymous) l,na)
+  | GApp (loc,GRef (_,ConstructRef cstr),l) ->
+      PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
   | _ -> raise Not_found
 
-(* Turn a closed cases pattern into a rawconstr *)
-let rec rawconstr_of_closed_cases_pattern_aux = function
+(* Turn a closed cases pattern into a glob_constr *)
+let rec glob_constr_of_closed_cases_pattern_aux = function
   | PatCstr (loc,cstr,[],Anonymous) ->
-      RRef (loc,ConstructRef cstr)
+      GRef (loc,ConstructRef cstr)
   | PatCstr (loc,cstr,l,Anonymous) ->
-      let ref = RRef (loc,ConstructRef cstr) in
-      RApp (loc,ref, List.map rawconstr_of_closed_cases_pattern_aux l)
+      let ref = GRef (loc,ConstructRef cstr) in
+      GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
 
-let rawconstr_of_closed_cases_pattern = function
+let glob_constr_of_closed_cases_pattern = function
   | PatCstr (loc,cstr,l,na) ->
-      na,rawconstr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
+      na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 1ab5ee7a55..95305d58c2 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -50,29 +50,29 @@ type 'a cast_type =
   | CastConv of cast_kind * 'a
   | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
 
-type rawconstr =
-  | RRef of (loc * global_reference)
-  | RVar of (loc * identifier)
-  | REvar of loc * existential_key * rawconstr list option
-  | RPatVar of loc * (bool * patvar) (** Used for patterns only *)
-  | RApp of loc * rawconstr * rawconstr list
-  | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
-  | RProd of loc * name * binding_kind * rawconstr * rawconstr
-  | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
-  | RLetTuple of loc * name list * (name * rawconstr option) *
-      rawconstr * rawconstr
-  | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
-  | RRec of loc * fix_kind * identifier array * rawdecl list array *
-      rawconstr array * rawconstr array
-  | RSort of loc * rawsort
-  | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * rawconstr cast_type
-  | RDynamic of loc * Dyn.t
-
-and rawdecl = name * binding_kind * rawconstr option * rawconstr
-
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
+type glob_constr =
+  | GRef of (loc * global_reference)
+  | GVar of (loc * identifier)
+  | GEvar of loc * existential_key * glob_constr list option
+  | GPatVar of loc * (bool * patvar) (** Used for patterns only *)
+  | GApp of loc * glob_constr * glob_constr list
+  | GLambda of loc * name * binding_kind *  glob_constr * glob_constr
+  | GProd of loc * name * binding_kind * glob_constr * glob_constr
+  | GLetIn of loc * name * glob_constr * glob_constr
+  | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
+  | GLetTuple of loc * name list * (name * glob_constr option) *
+      glob_constr * glob_constr
+  | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
+  | GRec of loc * fix_kind * identifier array * glob_decl list array *
+      glob_constr array * glob_constr array
+  | GSort of loc * rawsort
+  | GHole of (loc * Evd.hole_kind)
+  | GCast of loc * glob_constr * glob_constr cast_type
+  | GDynamic of loc * Dyn.t
+
+and glob_decl = name * binding_kind * glob_constr option * glob_constr
+
+and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
@@ -81,42 +81,42 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern)
+and tomatch_tuple = (glob_constr * predicate_pattern)
 
 and tomatch_tuples = tomatch_tuple list
 
-and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
+and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
 
 and cases_clauses = cases_clause list
 
 val cases_predicate_names : tomatch_tuples -> name list
 
-val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
+val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr
 
 (* Ensure traversal from left to right *)
-val map_rawconstr_left_to_right :
-  (rawconstr -> rawconstr) -> rawconstr -> rawconstr
+val map_glob_constr_left_to_right :
+  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
 
 (*
-val map_rawconstr_with_binders_loc : loc ->
+val map_glob_constr_with_binders_loc : loc ->
   (identifier -> 'a -> identifier * 'a) ->
-  ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
+  ('a -> glob_constr -> glob_constr) -> 'a -> glob_constr -> glob_constr
 *)
 
-val fold_rawconstr : ('a -> rawconstr -> 'a) -> 'a -> rawconstr -> 'a
-val iter_rawconstr : (rawconstr -> unit) -> rawconstr -> unit
-val occur_rawconstr : identifier -> rawconstr -> bool
-val free_rawvars : rawconstr -> identifier list
-val loc_of_rawconstr : rawconstr -> loc
+val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
+val occur_glob_constr : identifier -> glob_constr -> bool
+val free_glob_vars : glob_constr -> identifier list
+val loc_of_glob_constr : glob_constr -> loc
 
-(** Conversion from rawconstr to cases pattern, if possible
+(** Conversion from glob_constr to cases pattern, if possible
     
     Take the current alias as parameter, 
     @raise Not_found if translation is impossible *)
 
-val cases_pattern_of_rawconstr : name -> rawconstr -> cases_pattern
+val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
 
-val rawconstr_of_closed_cases_pattern : cases_pattern -> name * rawconstr
+val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
 
 (** {6 Reduction expressions} *)