Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 718 deletions

diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
deleted file mode 100644
index 92396af5..00000000
--- a/contrib/funind/rawtermops.ml
+++ /dev/null
@@ -1,718 +0,0 @@
-open Pp 
-open Rawterm
-open Util
-open Names
-(* Ocaml 3.06 Map.S does not handle is_empty *)
-let idmap_is_empty m = m = Idmap.empty
-
-(* 
-   Some basic functions to rebuild rawconstr
-   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))
-
-(*
-  Some basic functions to decompose rawconstrs
-  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 
-  | 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 
-  | rt -> args,rt
-  in
-  raw_decompose_prod []
-
-let raw_compose_prod = 
-  List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
-
-let raw_compose_prod_or_letin = 
-  List.fold_left (
-      fun concl decl -> 
-	match decl with 
-	  | (n,None,Some t) -> mkRProd(n,t,concl)
-	  | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl)
-	  | _ -> assert false)
-
-let raw_decompose_prod_n n = 
-  let rec raw_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 
-	| rt -> args,rt
-  in
-  raw_decompose_prod n []
-
-
-let raw_decompose_prod_or_letin_n n = 
-  let rec raw_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 
-	| rt -> args,rt
-  in
-  raw_decompose_prod n []
-
-
-let raw_decompose_app = 
-  let rec decompose_rapp acc rt =
-(*     msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
-    match rt with 
-    | RApp(_,rt,rtl) -> 
-	decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
-    | rt -> rt,List.rev acc
-  in
-  decompose_rapp [] 
-
-
-
-
-(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) 
-let raw_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])
-
-(* [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])
-
-(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding 
-   to [P1 \/ ( .... \/ Pn)] 
-*) 
-let rec raw_make_or_list = function  
-  | [] -> raise (Invalid_argument "mk_or")
-  | [e] -> e
-  | e::l -> raw_make_or e (raw_make_or_list l)
-
-  
-let remove_name_from_mapping mapping na = 
-  match na with 
-    | Anonymous -> mapping 
-    | Name id -> Idmap.remove id mapping
-
-let change_vars = 
-  let rec change_vars mapping rt = 
-    match rt with 
-      | RRef _ -> rt 
-      | RVar(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,
-	       change_vars mapping rt',
-	       List.map (change_vars mapping) rtl
-	      )
-      | RLambda(loc,name,k,t,b) -> 
-	  RLambda(loc,
-		  name,
-		  k,
-		  change_vars mapping t,
-		  change_vars (remove_name_from_mapping mapping name) b
-		 )
-      | RProd(loc,name,k,t,b) -> 
-	  RProd(loc,
-		  name,
-	          k,
-		  change_vars mapping t,
-		  change_vars (remove_name_from_mapping mapping name) b
-		 )
-      | RLetIn(loc,name,def,b) -> 
-	  RLetIn(loc,
-		 name,
-		 change_vars mapping def,
-		 change_vars (remove_name_from_mapping mapping name) b
-		)
-      | RLetTuple(loc,nal,(na,rto),b,e) -> 
-	  let new_mapping = List.fold_left remove_name_from_mapping mapping nal in 
-	  RLetTuple(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,
-		 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,
-	      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"
-  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 
-    then br 
-    else (loc,idl,patl,change_vars new_mapping res)
-  in
-  change_vars 
-
-
-
-let rec alpha_pat excluded pat = 
-  match pat with 
-    | PatVar(loc,Anonymous) -> 
-	let new_id = Indfun_common.fresh_id excluded "_x" in 
-	PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty
-    | PatVar(loc,Name id) -> 
-	if List.mem id excluded 
-	then 
-	  let new_id = Nameops.next_ident_away id excluded in 
-	  PatVar(loc,Name new_id),(new_id::excluded),
-	(Idmap.add id new_id Idmap.empty)
-	else pat,excluded,Idmap.empty
-    | PatCstr(loc,constr,patl,na) -> 
-	let new_na,new_excluded,map = 
-	  match na with 
-	    | Name id when List.mem id excluded -> 
-		let new_id = Nameops.next_ident_away id excluded in 
-		Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
-	    | _ -> na,excluded,Idmap.empty
-	in 
-	let new_patl,new_excluded,new_map = 
-	  List.fold_left 
-	    (fun (patl,excluded,map) pat -> 
-	       let new_pat,new_excluded,new_map = alpha_pat excluded pat in 
-	       (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map)
-	    )
-	    ([],new_excluded,map)
-	    patl
-	in 
-	PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map
-
-let alpha_patl excluded patl  = 
-  let patl,new_excluded,map = 
-    List.fold_left 
-      (fun (patl,excluded,map) pat -> 
-	 let new_pat,new_excluded,new_map = alpha_pat excluded pat in 
-	 new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map)
-      )
-      ([],excluded,Idmap.empty)
-      patl
-  in 
-  (List.rev patl,new_excluded,map)
-
-
-
-  
-let raw_get_pattern_id pat acc = 
-  let rec get_pattern_id pat = 
-    match pat with 
-      | PatVar(loc,Anonymous) -> assert false
-      | PatVar(loc,Name id) -> 
-	  [id]
-      | PatCstr(loc,constr,patternl,_) -> 
-	  List.fold_right 
-	  (fun pat idl -> 
-	     let idl' = get_pattern_id pat in 
-	     idl'@idl
-	  )
-	    patternl 
-	    []
-  in
-  (get_pattern_id pat)@acc
-
-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) -> 
-	  let new_id = Nameops.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) -> 
-	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) -> 
-	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) -> 
-	let new_id = Nameops.next_ident_away id excluded in 
-	let t,b = 
-	  if new_id = id 
-	  then t,b
-	  else 
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in 
-	    (t,replace b)
-	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,Name id,k,t,b) -> 
-	let new_id = Nameops.next_ident_away id excluded in 
-	let new_excluded = new_id::excluded in 
-	let t,b = 
-	  if new_id = id 
-	  then t,b
-	  else 
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in 
-	    (t,replace b)
-	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) -> 
-	let new_id = Nameops.next_ident_away id excluded in 
-	let t,b = 
-	  if new_id = id 
-	  then t,b
-	  else 
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in 
-	    (t,replace b)
-	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 
-	RLetIn(loc,Name new_id,new_t,new_b)
-
-
-    | RLetTuple(loc,nal,(na,rto),t,b) -> 
-	let rev_new_nal,new_excluded,mapping = 
-	  List.fold_left 
-	    (fun (nal,excluded,mapping) na -> 
-	       match na with 
-		 | Anonymous -> (na::nal,excluded,mapping)
-		 | Name id ->  
-		     let new_id = Nameops.next_ident_away id excluded in 
-		     if new_id = id 
-		     then 
-		       na::nal,id::excluded,mapping 
-		     else 
-		       (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping)
-	    )
-	    ([],excluded,Idmap.empty)
-	    nal
-	in
-	let new_nal = List.rev rev_new_nal in 
-	let new_rto,new_t,new_b = 
-	  if idmap_is_empty mapping
-	  then rto,t,b
-	  else let replace = change_vars mapping in 
-	  (Option.map replace rto, t,replace b)
-	in
-	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) -> 
-	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,
-	    (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,
-	     alpha_rt excluded f,
-	     List.map (alpha_rt excluded) args
-	    )
-  in 
-  new_rt
-
-and alpha_br excluded (loc,ids,patl,res) = 
-  let new_patl,new_excluded,mapping = alpha_patl excluded patl in 
-  let new_ids = List.fold_right raw_get_pattern_id new_patl [] in 
-  let new_excluded = new_ids@excluded in 
-  let renamed_res = change_vars mapping res in 
-  let new_res = alpha_rt new_excluded renamed_res in 
-  (loc,new_ids,new_patl,new_res)
-    
-(* 
-   [is_free_in id rt] checks if [id] is a free variable in [rt]
-*)
-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) ->
-	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) ->
-	(List.exists (fun (e,_) -> is_free_in e) el) ||
-	  List.exists is_free_in_br brl
-    | RLetTuple(_,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) ->
-	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"))
-  and is_free_in_br (_,ids,_,rt) =
-    (not (List.mem id ids)) && is_free_in rt
-  in
-  is_free_in
-      
-
-
-let rec pattern_to_term  = function
-  | PatVar(loc,Anonymous) -> assert false
-  | PatVar(loc,Name id) ->
-	mkRVar id
-  | PatCstr(loc,constr,patternl,_) ->
-      let cst_narg =
-	Inductiveops.mis_constructor_nargs_env
-	  (Global.env ())
-	  constr
-      in
-      let implicit_args =
-	Array.to_list
-	  (Array.init
-	     (cst_narg - List.length patternl)
-	     (fun _ -> mkRHole ())
-	  )
-      in
-      let patl_as_term =
-	List.map pattern_to_term patternl
-      in
-      mkRApp(mkRRef(Libnames.ConstructRef constr),
-	     implicit_args@patl_as_term
-	    )
-
-  
-
-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,
-	       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,
-		  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,
-		  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,
-		 name,
-		 replace_var_by_pattern def,
-		 replace_var_by_pattern b
-		)
-      | RLetTuple(_,nal,_,_,_) 
-	  when List.exists (function Name id -> id = x_id | _ -> false) nal  ->  
-	  rt
-      | RLetTuple(loc,nal,(na,rto),def,b) -> 
-	  RLetTuple(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,
-		 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,
-	      (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"))
-  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 
-    else (loc,idl,patl,replace_var_by_pattern res)
-  in
-  replace_var_by_pattern 
-
-
-
-
-(* checking unifiability of patterns *) 
-exception NotUnifiable  
-
-let rec are_unifiable_aux  = function 
-  | [] -> () 
-  | eq::eqs -> 
-      match eq with 
-	 | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs 
-	 | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> 
-	     if constructor2 <> constructor1 
-	     then raise NotUnifiable
-	     else 
-	       let eqs' = 
- 		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "are_unifiable_aux" 
-	       in
-	       are_unifiable_aux eqs'
-		 
-let are_unifiable pat1 pat2 = 
-  try 
-    are_unifiable_aux [pat1,pat2];
-    true
-  with NotUnifiable -> false
-
-
-let rec eq_cases_pattern_aux  = function 
-  | [] -> () 
-  | eq::eqs -> 
-      match eq with 
-	 | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs 
-	 | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> 
-	     if constructor2 <> constructor1 
-	     then raise NotUnifiable
-	     else 
-	       let eqs' = 
- 		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "eq_cases_pattern_aux" 
-	       in
-	       eq_cases_pattern_aux eqs'
-	 | _ -> raise NotUnifiable
-
-let eq_cases_pattern pat1 pat2 = 
-  try
-    eq_cases_pattern_aux [pat1,pat2];
-    true
-  with NotUnifiable -> false
-
-
-
-let ids_of_pat = 
-  let rec ids_of_pat ids = function 
-    | PatVar(_,Anonymous) -> ids 
-    | PatVar(_,Name id) -> Idset.add id ids 
-    | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl
-  in
-  ids_of_pat Idset.empty 
-  
-let id_of_name = function 
-  | Names.Anonymous -> id_of_string "x" 
-  | Names.Name x -> x
-
-(* TODO: finish Rec caes *)
-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) -> 
-          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) -> 
-          List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCases (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 _) -> []
-  in
-  (* build the set *)
-  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (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,
-	       zeta_normalize_term rt',
-	       List.map zeta_normalize_term rtl
-	      )
-      | RLambda(loc,name,k,t,b) -> 
-	  RLambda(loc,
-		  name,
-		  k,
-		  zeta_normalize_term t,
-		  zeta_normalize_term b
-		 )
-      | RProd(loc,name,k,t,b) -> 
-	  RProd(loc,
-		name, 		
-	        k,
-		zeta_normalize_term t,
-		zeta_normalize_term b
-		 )
-      | RLetIn(_,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,
-		    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,
-		 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,
-	      (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"))
-  and zeta_normalize_br (loc,idl,patl,res) = 
-    (loc,idl,patl,zeta_normalize_term res)
-  in
-  zeta_normalize_term 
-
-
-
-
-let expand_as = 
-  
-  let rec add_as map pat = 
-    match pat with 
-      | PatVar _ -> map 
-      | PatCstr(_,_,patl,Name id) -> 
-	  Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
-      | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
-  in 
-  let rec expand_as map rt = 
-    match rt with 
-      | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt 
-      | RVar(_,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),
-		    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),
-	      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,
-		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)
-  in
-  expand_as Idmap.empty