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

1 files changed, 208 insertions, 208 deletions

diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index e31f1452d9..f372fb017a 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)