Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 1012 insertions, 0 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
new file mode 100644
index 00000000..327198b9
--- /dev/null
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -0,0 +1,1012 @@
+open Printer
+open Pp
+open Names 
+open Term
+open Rawterm
+open Libnames
+open Indfun_common
+open Util
+open Rawtermops
+
+let observe strm =  
+  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  && false 
+  then Pp.msgnl strm 
+  else ()
+let observennl strm =  
+  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  &&false 
+  then Pp.msg strm 
+  else ()
+
+(* type binder_type =  *)
+(*   | Lambda  *)
+(*   | Prod  *)
+(*   | LetIn *)
+  
+(* type raw_context = (binder_type*name*rawconstr) list *)
+
+type binder_type =
+  | Lambda of name 
+  | Prod of name 
+  | LetIn of name
+(*   | LetTuple of name list * name  *)
+
+type raw_context = (binder_type*rawconstr) list
+
+
+(* 
+   compose_raw_context [(bt_1,n_1,t_1);......] rt returns 
+   b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the 
+   binders corresponding to the bt_i's
+*)
+let compose_raw_context = 
+  let compose_binder  (bt,t) acc =
+    match bt with 
+      | Lambda n -> mkRLambda(n,t,acc)
+      | Prod n -> mkRProd(n,t,acc)
+      | LetIn n -> mkRLetIn(n,t,acc)
+(*       | LetTuple (nal,na) ->  *)
+(* 	  RLetTuple(dummy_loc,nal,(na,None),t,acc) *)
+  in
+  List.fold_right compose_binder
+  
+
+(* 
+   The main part deals with building a list of raw constructor expressions
+   from the rhs of a fixpoint equation. 
+   
+   
+*)
+
+
+
+type 'a build_entry_pre_return = 
+    {
+      context : raw_context;  (* the binding context of the result *)
+      value : 'a; (* The value *)
+    }
+
+type 'a build_entry_return = 
+    {
+      result : 'a build_entry_pre_return list; 
+      to_avoid : identifier list
+    }
+
+
+(*
+  [combine_results combine_fun res1 res2] combine two results [res1] and [res2] 
+  w.r.t. [combine_fun].
+
+  Informally, both [res1] and [res2] are lists of "constructors"  [res1_1;...] 
+  and [res2_1,....] and we need to produce 
+  [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
+*)
+
+let combine_results 
+    (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return -> 
+      'c build_entry_pre_return
+    )  
+    (res1: 'a build_entry_return) 
+    (res2 : 'b build_entry_return) 
+    : 'c build_entry_return 
+    = 
+  let pre_result =     List.map 
+    ( fun res1 ->  (* for each result in arg_res *)
+	  List.map (* we add it in each args_res *) 
+	    (fun res2 -> 
+	       combine_fun res1 res2
+	    )
+	    res2.result
+      )
+      res1.result
+  in (* and then we flatten the map *)
+  {
+    result = List.concat pre_result; 
+    to_avoid = list_union res1.to_avoid res2.to_avoid
+  }
+    
+
+(* 
+   The combination function for an argument with a list of argument 
+*)
+
+let combine_args arg args = 
+  {
+    context = arg.context@args.context; 
+    (* Note that the binding context of [arg] MUST be placed before the one of 
+       [args] in order to preserve possible type dependencies 
+    *)
+    value = arg.value::args.value;
+  }
+
+
+let ids_of_binder =  function 
+  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
+  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]
+(*   | LetTuple(nal,_) ->  *)
+(*       map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *)
+
+let rec change_vars_in_binder mapping = function 
+    [] -> []
+  | (bt,t)::l ->
+      let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in 
+      (bt,change_vars mapping t)::
+	(if idmap_is_empty new_mapping
+	 then l 
+	 else change_vars_in_binder new_mapping l
+	)
+
+let rec replace_var_by_term_in_binder x_id term = function
+  | [] -> []
+  | (bt,t)::l -> 
+      (bt,replace_var_by_term x_id term t)::
+	if List.mem x_id (ids_of_binder bt) 
+	then l
+	else replace_var_by_term_in_binder x_id term l
+
+let add_bt_names bt = List.append (ids_of_binder bt)
+
+(* let rec replace_var_by_term_in_binder x_id term = function  *)
+(*   | [] -> []  *)
+(*   | (bt,Name id,t)::l when id_ord id x_id = 0 ->  *)
+(*       (bt,Name id,replace_var_by_term x_id term t)::l *)
+(*   | (bt,na,t)::l ->  *)
+(*       (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l) *)
+
+(* let rec change_vars_in_binder mapping = function *)
+(*   | [] -> [] *)
+(*   | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> *)
+(*       (bt,na,change_vars mapping t):: l *)
+(*   | (bt,na,t)::l -> *)
+(*       (bt,na,change_vars mapping t):: *)
+(* 	(change_vars_in_binder mapping l) *)
+
+   
+(* let alpha_ctxt avoid b = *)
+(*   let rec alpha_ctxt = function *)
+(*     | [] -> [],b *)
+(*     | (bt,n,t)::ctxt -> *)
+(* 	let new_ctxt,new_b = alpha_ctxt ctxt in *)
+(* 	match n with *)
+(* 	  | Name id when List.mem id avoid -> *)
+(* 	      let new_id = Nameops.next_ident_away id avoid in *)
+(* 	      let mapping = Idmap.add id new_id Idmap.empty in *)
+(* 	      (bt,Name new_id,t):: *)
+(* 		(change_vars_in_binder mapping new_ctxt), *)
+(* 	      change_vars mapping new_b *)
+(* 	  | _ -> (bt,n,t)::new_ctxt,new_b *)
+(*   in *)
+(*   alpha_ctxt *)
+let apply_args ctxt body args = 
+  let need_convert_id avoid id = 
+    List.exists (is_free_in id) args || List.mem id avoid 
+  in 
+  let need_convert avoid  bt =  
+    List.exists (need_convert_id avoid) (ids_of_binder bt)
+  in
+(*   let add_name na avoid =  *)
+(*     match na with  *)
+(*       | Anonymous -> avoid  *)
+(*       | Name id -> id::avoid  *)
+(*   in *)
+  let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = 
+    match na with 
+       | Name id when List.mem id avoid -> 
+	   let new_id = Nameops.next_ident_away id avoid in 
+	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
+       | _ -> na,mapping,avoid
+  in
+  let next_bt_away bt (avoid:identifier list) = 
+    match bt with 
+      | LetIn na -> 
+	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in 
+	  LetIn new_na,mapping,new_avoid
+      | Prod na -> 
+	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in 
+	  Prod new_na,mapping,new_avoid
+      | Lambda na -> 
+	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in 
+	  Lambda new_na,mapping,new_avoid
+(*       | LetTuple (nal,na) ->  *)
+(* 	  let rev_new_nal,mapping,new_avoid =  *)
+(* 	    List.fold_left *)
+(* 	      (fun (nal,mapping,(avoid:identifier list)) na ->  *)
+(* 		 let new_na,new_mapping,new_avoid = next_name_away na mapping avoid in *)
+(* 		 (new_na::nal,new_mapping,new_avoid) *)
+(* 	      ) *)
+(* 	      ([],Idmap.empty,avoid) *)
+(* 	      nal *)
+(* 	  in  *)
+(* 	  (LetTuple(List.rev rev_new_nal,na),mapping,new_avoid) *)
+  in
+  let rec do_apply avoid ctxt body args = 
+    match ctxt,args with  
+      | _,[] -> (* No more args *)
+	  (ctxt,body)
+      | [],_ -> (* no more fun *)
+	  let f,args' = raw_decompose_app body in
+	  (ctxt,mkRApp(f,args'@args))
+      | (Lambda Anonymous,t)::ctxt',arg::args' -> 
+	  do_apply avoid ctxt' body args'
+      | (Lambda (Name id),t)::ctxt',arg::args' -> 
+	  let new_avoid,new_ctxt',new_body,new_id = 
+	    if need_convert_id avoid id 
+	    then 
+	      let new_avoid =  id::avoid in 
+	      let new_id = Nameops.next_ident_away id new_avoid in 
+	      let new_avoid' = new_id :: new_avoid in 
+	      let mapping = Idmap.add id new_id Idmap.empty in 
+	      let new_ctxt' = change_vars_in_binder mapping ctxt' in 
+	      let new_body = change_vars mapping body in 
+	      new_avoid',new_ctxt',new_body,new_id
+	    else 
+	      id::avoid,ctxt',body,id 
+	  in
+	  let new_body = replace_var_by_term new_id arg new_body in
+	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
+	  do_apply avoid new_ctxt' new_body args'
+      | (bt,t)::ctxt',_ -> 
+	  let new_avoid,new_ctxt',new_body,new_bt = 
+	    let new_avoid = add_bt_names bt avoid in 
+	    if need_convert avoid bt 
+	    then 
+	      let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in 
+	      (
+		new_avoid,
+		change_vars_in_binder mapping ctxt',
+		change_vars mapping body,
+		new_bt
+	     )
+	    else new_avoid,ctxt',body,bt
+	  in
+	  let new_ctxt',new_body = 
+	    do_apply new_avoid new_ctxt' new_body args 
+	  in
+	  (new_bt,t)::new_ctxt',new_body
+  in 
+  do_apply []  ctxt body args
+
+
+let combine_app f args = 
+  let new_ctxt,new_value = apply_args f.context f.value args.value in 
+  { 
+    (* Note that the binding context of [args] MUST be placed before the one of 
+       the applied value in order to preserve possible type dependencies 
+    *)
+
+      context = args.context@new_ctxt;
+      value = new_value;
+  }
+
+let combine_lam n t b = 
+  {
+    context = []; 
+    value = mkRLambda(n, compose_raw_context t.context t.value, 
+		      compose_raw_context b.context b.value )
+  }
+
+
+
+let combine_prod n t b = 
+  { context = t.context@((Prod n,t.value)::b.context); value = b.value}
+
+let combine_letin n t b = 
+  { context = t.context@((LetIn n,t.value)::b.context); value = b.value}
+
+(* let combine_tuple nal na b in_e =  *)
+(*   {  *)
+(*     context = b.context@(LetTuple(nal,na),b.value)::in_e.context;  *)
+(*     value = in_e.value *)
+(*   } *)
+
+let mk_result ctxt value avoid = 
+  { 
+    result = 
+      [{context = ctxt;
+	value = value}]
+	;
+    to_avoid = avoid
+  }
+
+
+let make_discr_match_el  = 
+  List.map (fun e -> (e,(Anonymous,None)))
+
+let coq_True_ref = 
+  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "True")
+
+let coq_False_ref = 
+  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "False")
+
+let make_discr_match_brl i = 
+  list_map_i 
+    (fun j (_,idl,patl,_) -> 
+       if j=i
+       then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref))
+       else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref))
+    )
+    0 
+    
+let make_discr_match brl = 
+  fun el i -> 
+  mkRCases(None,
+	   make_discr_match_el el,
+	   make_discr_match_brl i brl)
+  
+
+
+let rec make_pattern_eq_precond id e pat : identifier * (binder_type * Rawterm.rawconstr) list = 
+  match pat with 
+    | PatVar(_,Anonymous) -> assert false 
+    | PatVar(_,Name x) -> 
+	id,[Prod (Name x),mkRHole ();Prod Anonymous,raw_make_eq (mkRVar x) e]
+    | PatCstr(_,constr,patternl,_) -> 
+	let new_id,new_patternl,patternl_eq_precond = 
+	  List.fold_right 
+	    (fun pat' (id,new_patternl,preconds) -> 
+	       match pat' with 
+		 | PatVar (_,Name id) -> (id,id::new_patternl,preconds)
+		 | _ -> 
+		     let new_id = Nameops.lift_ident id in 
+		     let new_id',pat'_precond = 
+		       make_pattern_eq_precond new_id (mkRVar id) pat' 
+		     in
+		     (new_id',id::new_patternl,preconds@pat'_precond)
+	    )
+	    patternl
+	    (id,[],[])
+	in
+	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 cst_as_term =      
+	  mkRApp(mkRRef(Libnames.ConstructRef constr),
+		 implicit_args@(List.map mkRVar new_patternl)
+		)
+	in
+	let precond' = 
+	  (Prod Anonymous, raw_make_eq cst_as_term  e)::patternl_eq_precond 
+	in
+	let precond'' = 
+	  List.fold_right 
+	    (fun id acc ->
+	       (Prod (Name id),(mkRHole ()))::acc
+	    )
+	    new_patternl
+	    precond'
+	in
+	new_id,precond''
+
+let pr_name = function
+  | Name id -> Ppconstr.pr_id id
+  | Anonymous -> str "_"
+
+let make_pattern_eq_precond id e pat = 
+  let res = make_pattern_eq_precond id e pat in 
+  observe 
+    (prlist_with_sep spc  
+       (function (Prod na,t) -> 
+	  str "forall " ++ pr_name na ++ str ":" ++ pr_rawconstr t
+	| _ -> assert false
+       )
+       (snd res)
+    );
+  res
+
+
+let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return = 
+(*   Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
+  match rt with 
+    | RRef _ | RVar _ | REvar _ | RPatVar _     | RSort _  | RHole _  -> 
+	mk_result [] rt avoid
+    | RApp(_,_,_) ->
+	let f,args = raw_decompose_app rt in
+	let args_res : (rawconstr list) build_entry_return =
+	  List.fold_right
+	    (fun arg ctxt_argsl ->
+	       let arg_res = build_entry_lc  funnames ctxt_argsl.to_avoid arg in
+	       combine_results combine_args  arg_res ctxt_argsl
+	    )
+	    args
+	    (mk_result [] [] avoid)
+	in
+	begin
+	  match f with
+	    | RVar(_,id) when Idset.mem id funnames ->
+		let res = fresh_id args_res.to_avoid "res" in
+		let new_avoid = res::args_res.to_avoid in
+		let res_rt = mkRVar res in 
+		let new_result = 
+		  List.map 
+		    (fun arg_res -> 
+		       let new_hyps = 
+			 [Prod (Name res),mkRHole ();
+			  Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
+		       in
+		       {context =  arg_res.context@new_hyps; value = res_rt } 
+		    )
+		    args_res.result
+		in 
+		{ result = new_result; to_avoid = new_avoid }
+	    | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ -> 
+		{
+		  args_res with 
+		    result = 
+		    List.map 
+		      (fun args_res -> 
+			 {args_res with value = mkRApp(f,args_res.value)})
+		      args_res.result
+		}
+	    | RApp _ -> assert false (* we have collected all the app *)
+       	    | RLetIn(_,n,t,b) -> 
+		let new_n,new_b,new_avoid = 
+		  match n with 
+		    | Name id when List.exists (is_free_in id) args -> 
+			(* need to alpha-convert the name *)
+			let new_id = Nameops.next_ident_away id avoid in 
+			let new_avoid = id:: avoid in
+			let new_b = 
+			  replace_var_by_term
+			    id
+			    (RVar(dummy_loc,id)) 
+			    b
+			in 
+			(Name new_id,new_b,new_avoid)
+		    | _ -> n,b,avoid
+		in
+		build_entry_lc 
+		  funnames 
+		  avoid
+		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
+	    | RCases _ | RLambda _  -> 
+		let f_res = build_entry_lc funnames  args_res.to_avoid f in
+		combine_results combine_app f_res  args_res
+	    | RDynamic _ ->error "Not handled RDynamic"
+	    | RCast _ -> error "Not handled RCast"
+	    | RRec _ -> error "Not handled RRec"
+	    | RIf _ -> error "Not handled RIf"
+	    | RLetTuple _ -> error "Not handled RLetTuple"
+	    | RProd _ -> error "Cannot apply a type"
+	end
+    | RLambda(_,n,t,b) ->
+	let b_res = build_entry_lc funnames avoid b in
+	let t_res = build_entry_lc funnames avoid t  in
+	let new_n = 
+	  match n with 
+	    | Name _ -> n 
+	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
+	in
+	combine_results (combine_lam new_n) t_res b_res
+    | RProd(_,n,t,b) ->
+	let b_res = build_entry_lc funnames avoid b in
+	let t_res = build_entry_lc funnames avoid t in
+	combine_results (combine_prod n) t_res b_res
+    | RLetIn(_,n,t,b) ->
+	let b_res = build_entry_lc funnames avoid b in
+	let t_res = build_entry_lc funnames avoid t in
+	combine_results (combine_letin n) t_res b_res
+    | RCases(_,_,el,brl) -> 
+	let make_discr = make_discr_match brl in 
+	build_entry_lc_from_case funnames make_discr el brl avoid
+    | RIf _ -> error "Not handled RIf"
+    | RLetTuple _ -> error "Not handled RLetTuple"
+    | RRec _ -> error "Not handled RRec"
+    | RCast _ -> error "Not handled RCast"
+    | RDynamic _ -> error "Not handled RDynamic"
+and build_entry_lc_from_case funname make_discr
+    (el:(Rawterm.rawconstr *
+	   (Names.name * (loc * Names.inductive * Names.name list) option) )
+       list)
+    (brl:(loc * identifier list * cases_pattern list * rawconstr) list) avoid : 
+    rawconstr build_entry_return = 
+  match el with 
+    | [] -> assert false (* matched on Nothing !*) 
+    | el -> 
+	let case_resl = 
+	    List.fold_right
+	    (fun (case_arg,_) ctxt_argsl ->
+	       let arg_res = build_entry_lc funname avoid case_arg  in
+	       combine_results combine_args arg_res ctxt_argsl
+	    )
+	    el
+	      (mk_result [] [] avoid)
+	in
+	let results =
+	  List.map 
+	    (build_entry_lc_from_case_term funname make_discr []  brl case_resl.to_avoid) 
+	    case_resl.result 
+	in 
+	{ 
+	  result = List.concat (List.map (fun r -> r.result) results);
+	  to_avoid = 
+	    List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+	} 
+
+and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+    matched_expr =
+  match brl with
+    | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
+    | br::brl' ->
+	let _,idl,patl,return = alpha_br avoid br in
+	let new_avoid  = idl@avoid in 
+(* 	let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
+(*  	if  (List.length patl) <> (List.length el) *)
+(* 	then error ("Pattern matching on product: not yet implemented"); *)
+	let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = 
+	  List.map 
+	    (fun pat -> 
+	       fun avoid pat'_as_term -> 
+		 let renamed_pat,_,_ = alpha_pat avoid pat in
+		 let pat_ids = get_pattern_id renamed_pat  in 
+		 List.fold_right 
+		   (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+		   pat_ids
+		   (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
+	    )
+	    patl
+	in
+	let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
+	  List.map 
+	    (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat') 
+	    patl
+	in
+	let brl'_res =
+	  build_entry_lc_from_case_term
+	    funname
+	    make_discr
+	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
+	    brl'
+	    avoid
+	    matched_expr
+	in
+(* 	let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in *)
+      	let those_pattern_preconds =
+(	  List.flatten
+	    (
+	    List.map2
+	      (fun pat e ->
+		 let this_pat_ids = ids_of_pat pat in 
+		 let pat_as_term = pattern_to_term pat in
+		 List.fold_right 
+		   (fun id  acc -> 
+		      if Idset.mem id this_pat_ids 
+		      then (Prod (Name id),mkRHole ())::acc
+		      else acc
+			
+		   )
+		   idl
+		   [(Prod Anonymous,raw_make_eq pat_as_term e)]
+	      )
+	      patl
+	      matched_expr.value
+	  )
+)
+	  @
+	    (if List.exists (function (unifl,neql) ->
+			       let (unif,eqs) = 
+				 List.split (List.map2 (fun x y -> x y) unifl patl)
+			       in
+			       List.for_all (fun x -> x) unif) patterns_to_prevent
+	     then 
+	       let i = List.length patterns_to_prevent in 
+	       [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i  )]
+	     else 
+	       []
+	    )
+	in
+	let return_res = build_entry_lc funname new_avoid return in
+	let this_branch_res =
+	  List.map
+	    (fun res  ->
+	       { context = 
+		   matched_expr.context@
+(* 		     ids@ *)
+		     those_pattern_preconds@res.context ;
+		 value = res.value}
+	    )
+	    return_res.result
+	in
+	{ brl'_res with result = this_branch_res@brl'_res.result }
+	  
+	  
+let is_res id = 
+  try
+    String.sub (string_of_id id) 0 3 = "res"
+  with Invalid_argument _ -> false 
+
+(* rebuild the raw constructors expression. 
+   eliminates some meaningless equalities, applies some rewrites......
+*)
+let rec rebuild_cons nb_args relname args crossed_types depth rt = 
+  match rt with 
+    | RProd(_,n,t,b) -> 
+	let not_free_in_t id = not (is_free_in id t) in 
+	let new_crossed_types = t::crossed_types in 
+	begin
+	  match t with 
+	    | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id ->
+		begin
+		  match args' with 
+		    | (RVar(_,this_relname))::args' -> 
+			let new_b,id_to_exclude =  
+			  rebuild_cons 
+			    nb_args relname
+			    args new_crossed_types
+			    (depth + 1) b
+			in 
+			let new_t = 
+			  mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) 
+			in mkRProd(n,new_t,new_b),
+			Idset.filter not_free_in_t id_to_exclude
+		    | _ -> (* the first args is the name of the function! *)
+			assert false 
+		end
+	    | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt]) 
+		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  
+		  -> 
+		let is_in_b = is_free_in id b in
+		let _keep_eq = 
+		  not (List.exists (is_free_in id) args) || is_in_b  || 
+		    List.exists (is_free_in id) crossed_types 
+		in 
+		let new_args = List.map (replace_var_by_term id rt) args in 
+		let subst_b = 
+		  if is_in_b then b else  replace_var_by_term id rt b 
+		in 
+		let new_b,id_to_exclude =  
+		  rebuild_cons 
+		    nb_args relname
+		    new_args new_crossed_types
+		    (depth + 1) subst_b
+		in 
+		mkRProd(n,t,new_b),id_to_exclude
+(*  		if keep_eq then *)
+(* 		  mkRProd(n,t,new_b),id_to_exclude *)
+(* 		else new_b, Idset.add id id_to_exclude *)
+	    | _ -> 
+		let new_b,id_to_exclude =  
+		  rebuild_cons 
+		    nb_args relname
+		    args new_crossed_types
+		    (depth + 1) b
+		in 
+		match n with
+		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Idset.remove id 
+			(Idset.filter not_free_in_t id_to_exclude)
+		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+	end
+    | RLambda(_,n,t,b) ->
+	begin
+(* 	  let not_free_in_t id = not (is_free_in id t) in  *)
+(* 	  let new_crossed_types = t :: crossed_types in  *)
+(* 	  let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in *)
+(* 	  match n with *)
+(* 	    | Name id when Idset.mem id id_to_exclude -> *)
+(* 		new_b, *)
+(* 		Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* 	    | _ ->  *)
+(* 		RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude *)
+	  let not_free_in_t id = not (is_free_in id t) in
+	  let new_crossed_types = t :: crossed_types in
+(* 	  let new_b,id_to_exclude = rebuild_cons relname (args new_crossed_types b in *)
+	  match n with
+	    | Name id ->
+		let new_b,id_to_exclude = 
+		  rebuild_cons 
+		    nb_args relname
+		    (args@[mkRVar id])new_crossed_types
+		    (depth + 1 ) b 
+		in
+		if Idset.mem id id_to_exclude && depth >= nb_args
+		then 
+		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+		else
+		  RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+	    | _ -> anomaly "Should not have an anonymous function here" 
+		(* We have renamed all the anonymous functions during alpha_renaming phase *)
+	  
+	end
+    | RLetIn(_,n,t,b) -> 
+	begin
+	  let not_free_in_t id = not (is_free_in id t) in 
+	  let new_b,id_to_exclude = 
+	    rebuild_cons 
+	      nb_args relname
+	      args (t::crossed_types)
+	      (depth + 1 ) b in
+	  match n with 
+	    | Name id when Idset.mem id id_to_exclude && depth >= nb_args  -> 
+		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+	    | _ -> RLetIn(dummy_loc,n,t,new_b),
+		Idset.filter not_free_in_t id_to_exclude
+	end
+    | RLetTuple(_,nal,(na,rto),t,b) -> 
+	assert (rto=None);
+	begin
+	  let not_free_in_t id = not (is_free_in id t) in 
+	  let new_t,id_to_exclude' = 
+	    rebuild_cons 
+	      nb_args
+	      relname 
+	      args (crossed_types) 
+	      depth t 
+	  in
+	  let new_b,id_to_exclude = 
+	    rebuild_cons 
+	      nb_args relname
+	      args (t::crossed_types) 
+	      (depth + 1) b 
+	  in
+(* 	  match n with  *)
+(* 	    | Name id when Idset.mem id id_to_exclude ->  *)
+(* 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* 	    | _ -> *)
+	  RLetTuple(dummy_loc,nal,(na,None),t,new_b),
+		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
+
+	end
+
+    | _ -> mkRApp(mkRVar  relname,args@[rt]),Idset.empty
+
+
+let rebuild_cons nb_args relname args crossed_types rt = 
+  observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ 
+		 str "nb_args := " ++ str (string_of_int nb_args));
+  let res = 
+    rebuild_cons nb_args relname args crossed_types 0 rt 
+  in
+  observe (str " leads to "++ pr_rawconstr (fst res));
+  res
+
+let rec compute_cst_params relnames params = function 
+  | RRef _ | RVar _ | REvar _ | RPatVar _ -> params
+  | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+      compute_cst_params_from_app [] (params,rtl)
+  | RApp(_,f,args) -> 
+      List.fold_left (compute_cst_params relnames) params (f::args)
+  | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
+      let t_params = compute_cst_params relnames params t in 
+      compute_cst_params relnames t_params b
+  | RCases _ -> params  (* If there is still cases at this point they can only be 
+			discriminitation ones *)
+  | RSort _ -> params
+  | RHole _ -> params
+  | RIf _ | RRec _ | RCast _ | RDynamic _  ->
+      raise (UserError("compute_cst_params", str "Not handled case"))
+and compute_cst_params_from_app acc (params,rtl) = 
+  match params,rtl with 
+    | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
+    | ((Name id,_,is_defined) as param)::params',(RVar(_,id'))::rtl' 
+	when id_ord id id' == 0 && not is_defined -> 
+	compute_cst_params_from_app (param::acc) (params',rtl')
+    | _  -> List.rev acc 
+   
+let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) list array) csts =  
+  let rels_params = 
+    Array.mapi 
+      (fun i args -> 
+	 List.fold_left 
+	   (fun params (_,cst) -> compute_cst_params relnames params cst) 
+	   args
+	   csts.(i)
+      )
+      args
+  in 
+  let l = ref [] in 
+  let _ = 
+    try 
+      list_iter_i
+	(fun i ((n,nt,is_defined) as param) -> 
+	   if array_for_all 
+	     (fun l -> 
+		let (n',nt',is_defined') = List.nth l i in 
+		n = n' && Topconstr.eq_rawconstr nt nt' && is_defined = is_defined')
+	     rels_params
+	   then 
+	     l := param::!l
+	) 
+	rels_params.(0)
+    with _ -> 
+      ()
+  in 
+  List.rev !l
+
+(*      (Topconstr.CProdN
+	 (dummy_loc,
+	  [[(dummy_loc,Anonymous)],returned_types.(i)],
+	  Topconstr.CSort(dummy_loc, RProp Null )
+	 )
+      )
+*)
+let rec rebuild_return_type rt = 
+  match rt with 
+    | Topconstr.CProdN(loc,n,t') -> 
+	Topconstr.CProdN(loc,n,rebuild_return_type t') 
+    | Topconstr.CArrow(loc,t,t') -> 
+	Topconstr.CArrow(loc,t,rebuild_return_type t')
+    | Topconstr.CLetIn(loc,na,t,t') -> 
+	Topconstr.CLetIn(loc,na,t,rebuild_return_type t') 
+    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc, RProp Null))
+
+
+let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)  returned_types (rtl:rawconstr list) =
+(*   Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *)
+  let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
+  let funnames = Array.of_list funnames in  
+  let funsargs = Array.of_list funsargs in 
+  let returned_types = Array.of_list returned_types in
+  let rtl_alpha = List.map (function rt ->  (alpha_rt [] rt) ) rtl in
+  let rta = Array.of_list rtl_alpha in
+  let relnames = Array.map mk_rel_id funnames in
+  let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in 
+  let resa = Array.map (build_entry_lc funnames_as_set []) rta in 
+  let constr i res = 
+    List.map 
+      (function result (* (args',concl') *) -> 
+	 let rt = compose_raw_context result.context result.value in 
+	 let nb_args = List.length funsargs.(i) in 
+(* 	 Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+	 fst (
+	   rebuild_cons nb_args relnames.(i)
+(* 	     (List.map  *)
+(* 		(function  *)
+(* 		     (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__")  *)
+(* 		   | Name id, _,_ -> mkRVar id *)
+(* 		) *)
+(* 		funsargs.(i) *)
+(* 	     )  *)
+	     []
+	     []
+	     rt 
+	 )
+      ) 
+      res.result 
+  in 
+  let next_constructor_id = ref (-1) in 
+  let mk_constructor_id i = 
+    incr next_constructor_id;
+    id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+  in
+  let rel_constructors i rt : (identifier*rawconstr) list = 
+    List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
+  in
+  let rel_constructors = Array.mapi rel_constructors resa in
+  let rels_params = 
+    if parametrize 
+    then
+      compute_params_name relnames_as_set funsargs  rel_constructors 
+    else []
+  in
+  let nrel_params = List.length rels_params in
+  let rel_constructors = 
+    Array.map (List.map 
+    (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
+    rel_constructors
+  in
+  let rel_arity i funargs = 
+    let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list  = 
+      (snd (list_chop nrel_params funargs))
+    in 
+    List.fold_right
+      (fun (n,t,is_defined) acc -> 
+	 if is_defined
+	 then 
+	   Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t,
+			    acc)
+	 else
+	   Topconstr.CProdN
+	   (dummy_loc,
+	    [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t],
+	    acc
+	   )
+      )
+      rel_first_args
+      (rebuild_return_type returned_types.(i))
+(*       (Topconstr.CProdN *)
+(* 	 (dummy_loc, *)
+(* 	  [[(dummy_loc,Anonymous)],returned_types.(i)], *)
+(* 	  Topconstr.CSort(dummy_loc, RProp Null ) *)
+(* 	 ) *)
+(* ) *)
+  in
+  let rel_arities = Array.mapi rel_arity funsargs in
+  let old_rawprint = !Options.raw_print in 
+  Options.raw_print := true;
+  let rel_params =  
+    List.map 
+      (fun (n,t,is_defined) -> 
+	 if is_defined 
+	 then
+	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t)
+	 else
+	 Topconstr.LocalRawAssum 
+	   ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t)
+      )
+      rels_params
+  in 
+  let ext_rels_constructors = 
+    Array.map (List.map 
+      (fun (id,t) -> 
+	 false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t)
+      ))
+      rel_constructors
+  in
+  let rel_ind i ext_rel_constructors = 
+    (dummy_loc,relnames.(i)),
+    None,
+    rel_params,
+    rel_arities.(i),
+    ext_rel_constructors
+  in
+  let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
+  let rel_inds = Array.to_list ext_rel_constructors in 
+  let _ = 
+    observe (
+      str "Inductive" ++ spc () ++
+	prlist_with_sep 
+	(fun () -> fnl ()++spc () ++ str "with" ++ spc ()) 
+	(function ((_,id),_,params,ar,constr) -> 
+	   Ppconstr.pr_id id ++ spc () ++ 
+	     Ppconstr.pr_binders params ++ spc () ++
+	     str ":" ++ spc () ++ 
+	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ 
+	     prlist_with_sep 
+	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ())
+	     (function (_,((_,id),t)) -> 
+		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++
+		  Ppconstr.pr_lconstr_expr t)
+	     constr
+	)
+	rel_inds
+    )
+  in
+  let old_implicit_args = Impargs.is_implicit_args ()
+  and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
+  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+  Impargs.make_implicit_args false;
+  Impargs.make_strict_implicit_args false;
+  Impargs.make_contextual_implicit_args false;
+  try 
+    Options.silently (Command.build_mutual rel_inds) true;
+    Impargs.make_implicit_args old_implicit_args;
+    Impargs.make_strict_implicit_args old_strict_implicit_args;
+    Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+    Options.raw_print := old_rawprint;
+  with
+    | UserError(s,msg) -> 
+	Impargs.make_implicit_args old_implicit_args;
+	Impargs.make_strict_implicit_args old_strict_implicit_args;
+	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+	Options.raw_print := old_rawprint;
+	let msg = 		     
+	  str "while trying to define"++ spc () ++
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+	    msg
+	in
+	observe (msg);
+	raise 
+	  (UserError(s, msg))
+    | e -> 
+	Impargs.make_implicit_args old_implicit_args;
+	Impargs.make_strict_implicit_args old_strict_implicit_args;
+	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+	Options.raw_print := old_rawprint;
+	let msg = 		     
+	  str "while trying to define"++ spc () ++
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+	    Cerrors.explain_exn e
+	in
+ 	observe msg;
+	raise 
+	  (UserError("",msg))
+
+