Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 1262 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
deleted file mode 100644
index 09b7fbdf..00000000
--- a/contrib/funind/rawterm_to_relation.ml
+++ /dev/null
@@ -1,1262 +0,0 @@
-open Printer
-open Pp
-open Names 
-open Term
-open Rawterm
-open Libnames
-open Indfun_common
-open Util
-open Rawtermops
-
-let observe strm =  
-  if do_observe ()
-  then Pp.msgnl strm 
-  else ()
-let observennl strm =  
-  if do_observe ()
-  then Pp.msg strm 
-  else ()
-
-
-type binder_type =
-  | Lambda of name 
-  | Prod of name 
-  | LetIn of 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)
-  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]
-
-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 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 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
-  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 mk_result ctxt value avoid = 
-  { 
-    result = 
-      [{context = ctxt;
-	value = value}]
-	;
-    to_avoid = avoid
-  }
-(*************************************************
-  Some functions to deal with overlapping patterns 
-**************************************************)
-
-let coq_True_ref = 
-  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "True")
-
-let coq_False_ref = 
-  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "False")
-
-(*
-  [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
-  (the list of expresions on which we will do the matching)
- *) 
-let make_discr_match_el  = 
-  List.map (fun e -> (e,(Anonymous,None)))
-
-(*
-  [make_discr_match_brl i \[pat_1,...,pat_n\]]  constructs a discrimination pattern matching on the ith expression. 
-  that is. 
-  match ?????? with \\
-  | pat_1 => False  \\
-  | pat_{i-1} => False \\
-  | pat_i => True \\
-  | pat_{i+1} => False \\
-  \vdots 
-  | pat_n => False
-  end
-*)
-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 
-(* 
-   [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff 
-   brl_{i} is the first branch matched by [el] 
-
-   Used when we want to simulate the coq pattern matching algorithm
-*)
-let make_discr_match brl = 
-  fun el i -> 
-  mkRCases(None,
-	   make_discr_match_el el,
-	   make_discr_match_brl i brl)
-
-let pr_name = function
-  | Name id -> Ppconstr.pr_id id
-  | Anonymous -> str "_"
-
-(**********************************************************************)
-(*  functions used to build case expression from lettuple and if ones *)
-(**********************************************************************)		
-
-(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)	  
-let build_constructors_of_type ind' argl = 
-  let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
-  let npar = mib.Declarations.mind_nparams in
-  Array.mapi (fun i _ ->
-		let construct = ind',i+1 in 
-		let constructref = ConstructRef(construct) in 
-		let _implicit_positions_of_cst =
-		  Impargs.implicits_of_global constructref
-		in
-		let cst_narg = 
-		  Inductiveops.mis_constructor_nargs_env
-		    (Global.env ())
-		    construct
-		in 
-		let argl = 
-		  if argl = [] 
-		  then
- 		    Array.to_list 
-		      (Array.init (cst_narg - npar) (fun _ -> mkRHole ())
-		      )
-		  else argl
-		in
-		let pat_as_term = 
-		  mkRApp(mkRRef (ConstructRef(ind',i+1)),argl)
-		in
-		cases_pattern_of_rawconstr Anonymous pat_as_term
-	     )
-    ind.Declarations.mind_consnames
-
-(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
-let rec find_type_of nb b = 
-  let f,_ = raw_decompose_app b in 
-  match f with 
-    | RRef(_,ref) -> 
-	begin 
-	  let ind_type  = 
-	    match ref with 
-	      | VarRef _ | ConstRef _ -> 
-		  let constr_of_ref = constr_of_global ref in  
-		  let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in 
-		  let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in 
-		  let ret_type,_ = decompose_app ret_type in 
-		  if not (isInd ret_type) then 
-		    begin
-(* 		      Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *)
-		      raise (Invalid_argument "not an inductive")
-		    end;
-		  destInd ret_type
-	      | IndRef ind -> ind
-	      | ConstructRef c -> fst c 
-	  in
-	  let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in 
-	  if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
-	  then raise (Invalid_argument "find_type_of : not a valid inductive");
-	  ind_type	   
-	end
-    | RCast(_,b,_) -> find_type_of nb b 
-    | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
-    | _ -> raise (Invalid_argument "not a ref")
-    
-
-
-
-(******************)
-(* Main functions *)
-(******************)
-
-
-
-let raw_push_named (na,raw_value,raw_typ) env = 
-  match na with 
-    | Anonymous -> env 
-    | Name id -> 
-	let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in 
-	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in 
-	Environ.push_named (id,value,typ) env
-
-
-let add_pat_variables pat typ env : Environ.env = 
-  let rec add_pat_variables env pat typ  : Environ.env = 
-    observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
-
-    match pat with 
-      | PatVar(_,na) -> Environ.push_rel (na,None,typ) env 
-      | PatCstr(_,c,patl,na) -> 
-	  let Inductiveops.IndType(indf,indargs) = 
-	    try Inductiveops.find_rectype env Evd.empty typ
-	    with Not_found -> assert false 
-	  in
-	  let constructors = Inductiveops.get_constructors env indf in 
-	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in 
-	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in 
-	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) 
-  in
-  let new_env = add_pat_variables  env pat typ in 
-  let res =
-    fst (
-      Sign.fold_rel_context
-	(fun (na,v,t) (env,ctxt) ->
-	 match na with
-	   | Anonymous -> assert false
-	   | Name id ->
-	       let new_t =  substl ctxt t in
-	       let new_v = Option.map (substl ctxt) v in
-	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
-			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
-			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
-			  Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
-			  Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
-		       );
-	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
-      )
-	(Environ.rel_context new_env)
-	~init:(env,[])
-    )
-  in
-  observe (str "new var env := " ++ Printer.pr_named_context_of res);
-  res
-
-
-
-
-let rec pattern_to_term_and_type env typ  = 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 Inductiveops.IndType(indf,indargs) = 
-	try Inductiveops.find_rectype env Evd.empty typ
-	with Not_found -> assert false 
-      in
-      let constructors = Inductiveops.get_constructors env indf in 
-      let constructor  = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in 
-      let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in 
-      let _,cstl = Inductiveops.dest_ind_family indf in 
-      let csta = Array.of_list cstl in 
-      let implicit_args =
-	Array.to_list
-	  (Array.init
-	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i))
-	  )
-      in
-      let patl_as_term =
-	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
-      in
-      mkRApp(mkRRef(ConstructRef constr),
-	     implicit_args@patl_as_term
-	    )
-
-(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) 
-   of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the 
-   corresponding graphs. 
-
-
-   The idea to transform a term [t] into a list of constructors [lc] is the following:
-   \begin{itemize} 
-   \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding 
-   to [body] and add (bind x. _) to each elements of [lc]
-   \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames) 
-   then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], 
-   then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn], 
-   [g c1 ... cn] is an element of [lc]
-   \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then 
-   compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], 
-   then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
-   create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
-   \item if the term is a cast just treat its body part
-   \item 
-   if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case 
-   and concatenate them (informally, each branch of a match produces a new constructor)
-   \end{itemize}
-   
-   WARNING: The terms constructed here are only USING the rawconstr syntax but are highly bad formed. 
-   We must wait to have complete all the current calculi to set the recursive calls. 
-   At this point, each term [f t1 ... tn]  (where f appears in [funnames]) is replaced by 
-   a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later. 
-   We in fact not create a constructor list since then end of each constructor has not the expected form 
-   but only the value of the function 
-*)
-
-
-let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return = 
-  observe (str " Entering : " ++ Printer.pr_rawconstr rt);
-  match rt with 
-    | RRef _ | RVar _ | REvar _ | RPatVar _     | RSort _  | RHole _  -> 
-	(* do nothing (except changing type of course) *)
-	mk_result [] rt avoid 
-    | RApp(_,_,_) ->
-	let f,args = raw_decompose_app rt in
-	let args_res : (rawconstr list) build_entry_return =
-	  List.fold_right (* create the arguments lists of constructors and combine them *)
-	    (fun arg ctxt_argsl ->
-	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
-	       combine_results combine_args arg_res ctxt_argsl
-	    )
-	    args
-	    (mk_result [] [] avoid)
-	in
-	begin
-	  match f with
-	    | RVar(_,id) when Idset.mem id funnames ->
-		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
-		   then we create a fresh variable [res], 
-		   add [res] and its "value" (i.e. [res v1 ... vn]) to each 
-		   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and 
-		   a pseudo value "v1 ... vn". 
-		   The "value" of this branch is then simply [res]
-		*)
-		let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in 
-		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in 
-		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
-		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),res_raw_type;
-			  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 _ -> 
-		(* if have [g t1 ... tn] with [g] not appearing in [funnames] 
-		   then  
-		   foreach [ctxt,v1 ... vn] in [args_res] we return  
-		   [ctxt, g v1 .... vn]
-		*)
-		{
-		  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 in [raw_decompose_app] *)
-       	    | RLetIn(_,n,t,b) -> 
-		(* if we have [(let x := v in b) t1 ... tn] , 
-		   we discard our work and compute the list of constructor for 
-		   [let x = v in (b t1 ... tn)] up to alpha conversion 
-		*)
-		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 
-		  env
-		  funnames 
-		  avoid
-		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
-	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ -> 
-		(* we have [(match e1, ...., en with ..... end) t1 tn]
-		   we first compute the result from the case and 
-		   then combine each of them with each of args one
-		*)
-		let f_res = build_entry_lc env funnames args_res.to_avoid f in
-		combine_results combine_app f_res  args_res
-	    | RDynamic _ ->error "Not handled RDynamic" 
-	    | RCast(_,b,_) -> 
-		(* for an applied cast we just trash the cast part 
-		   and restart the work. 
-
-		   WARNING: We need to restart since [b] itself should be an application term
-		*)
-		build_entry_lc env funnames avoid (mkRApp(b,args))
-	    | RRec _ -> error "Not handled RRec"
-	    | RProd _ -> error "Cannot apply a type"
-	end (* end of the application treatement *) 
-
-    | RLambda(_,n,_,t,b) ->
-	(* we first compute the list of constructor 
-	   corresponding to the body of the function, 
-	   then the one corresponding to the type 
-	   and combine the two result
-	*)
-	let t_res = build_entry_lc env funnames avoid t  in
-	let new_n = 
-	  match n with 
-	    | Name _ -> n 
-	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
-	in
-	let new_env = raw_push_named (new_n,None,t) env in
-	let b_res = build_entry_lc new_env funnames avoid b in
-	combine_results (combine_lam new_n) t_res b_res
-    | RProd(_,n,_,t,b) ->
-	(* we first compute the list of constructor 
-	   corresponding to the body of the function, 
-	   then the one corresponding to the type 
-	   and combine the two result
-	*)
-	let t_res = build_entry_lc env funnames avoid t in
-	let new_env = raw_push_named (n,None,t) env in
-	let b_res = build_entry_lc new_env funnames avoid b in
-	combine_results (combine_prod n) t_res b_res
-    | RLetIn(_,n,v,b) ->
-	(* we first compute the list of constructor 
-	   corresponding to the body of the function, 
-	   then the one corresponding to the value [t] 
-	   and combine the two result
-	*)
-	let v_res = build_entry_lc env funnames avoid v in
-	let v_as_constr = Pretyping.Default.understand Evd.empty env v in 
-	let v_type = Typing.type_of env Evd.empty v_as_constr in 
-	let new_env = 
-	  match n with
-	      Anonymous -> env
-	    | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env 
-	in
-	let b_res = build_entry_lc new_env funnames avoid b in
-	combine_results (combine_letin n) v_res b_res
-    | RCases(_,_,_,el,brl) -> 
-	(* we create the discrimination function 
-	   and treat the case itself 
-	*)
-	let make_discr = make_discr_match brl in 
-	build_entry_lc_from_case env funnames make_discr el brl avoid
-    | RIf(_,b,(na,e_option),lhs,rhs) -> 
-	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
-	let b_typ = Typing.type_of env Evd.empty b_as_constr in 
-	let (ind,_) =  
-	  try Inductiveops.find_inductive env Evd.empty b_typ 
-	  with Not_found -> 
-	    errorlabstrm "" (str "Cannot find the inductive associated to " ++ 
-			       Printer.pr_rawconstr b ++ str " in " ++
-			       Printer.pr_rawconstr rt ++ str ". try again with a cast")
-	in
-	let case_pats = build_constructors_of_type ind [] in 
-	assert (Array.length case_pats = 2);
-	let brl =
-	  list_map_i
-	    (fun i x -> (dummy_loc,[],[case_pats.(i)],x))
-	    0
-	    [lhs;rhs]
-	in
-	let match_expr =
-	  mkRCases(None,[(b,(Anonymous,None))],brl)
-	in
-	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
-	build_entry_lc env funnames avoid match_expr
-    | RLetTuple(_,nal,_,b,e) ->  
-	begin
-	  let nal_as_rawconstr =
-	    List.map
-	      (function
-		   Name id -> mkRVar id
-		 | Anonymous -> mkRHole ()
-	      )
-	      nal
-	  in
-	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
-	  let b_typ = Typing.type_of env Evd.empty b_as_constr in 
-	  let (ind,_) = 
-	    try Inductiveops.find_inductive env Evd.empty b_typ 
-	    with Not_found -> 
-	      errorlabstrm "" (str "Cannot find the inductive associated to " ++ 
-				 Printer.pr_rawconstr b ++ str " in " ++
-				 Printer.pr_rawconstr rt ++ str ". try again with a cast")
-	  in
-	  let case_pats = build_constructors_of_type ind nal_as_rawconstr in 
-	  assert (Array.length case_pats = 1);
-	  let br =
-	    (dummy_loc,[],[case_pats.(0)],e)
-	  in
-	  let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
-	  build_entry_lc env funnames avoid match_expr
-
-	end
-    | RRec _ -> error "Not handled RRec"
-    | RCast(_,b,_) -> 
-	build_entry_lc env funnames  avoid b
-    | RDynamic _ -> error "Not handled RDynamic"
-and build_entry_lc_from_case env funname make_discr
-    (el:tomatch_tuples)
-    (brl:Rawterm.cases_clauses) avoid : 
-    rawconstr build_entry_return = 
-  match el with 
-    | [] -> assert false (* this case correspond to match <nothing> with .... !*) 
-    | el -> 
-	(* this case correspond to 
-	   match el with brl end
-	   we first compute the list of lists corresponding to [el] and 
-	   combine them . 
-	   Then for each elemeent of the combinations, 
-	   we compute the result we compute one list per branch in [brl] and 
-	   finally we just concatenate those list 
-	*)
-	let case_resl = 
-	    List.fold_right
-	    (fun (case_arg,_) ctxt_argsl ->
-	       let arg_res = build_entry_lc env funname avoid case_arg  in
-	       combine_results combine_args arg_res ctxt_argsl
-	    )
-	    el
-	      (mk_result [] [] avoid)
-	in
-	(****** The next works only if the match is not dependent ****)
-	let types = 
-	  List.map (fun (case_arg,_) -> 
-		      let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in 
-		      Typing.type_of env Evd.empty case_arg_as_constr
-		   ) el
-	in
-	let results =
-	  List.map 
-	    (build_entry_lc_from_case_term
-	       env types
-	       funname (make_discr (* (List.map fst el) *))
-	       []  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 env types funname make_discr patterns_to_prevent brl avoid
-    matched_expr =
-  match brl with
-    | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
-    | br::brl' ->
-	(* alpha convertion to prevent name clashes *)
-	let _,idl,patl,return = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an indentifier *)
-	(* building a list of precondition stating that we are not in this branch 
-	   (will be used in the following recursive calls)
-	*)
-	let new_env = List.fold_right2 add_pat_variables patl types env in 
-	let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = 
-	  List.map2
-	    (fun pat typ -> 
-	       fun avoid pat'_as_term -> 
-		 let renamed_pat,_,_ = alpha_pat avoid pat in
-		 let pat_ids = get_pattern_id renamed_pat  in 
-		 let env_with_pat_ids = add_pat_variables pat typ new_env in 
-		   List.fold_right 
-		   (fun id acc -> 		 
-		      let typ_of_id = Typing.type_of env_with_pat_ids Evd.empty (mkVar id) in 
-		      let raw_typ_of_id = 
-			Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
-		      in
-		      mkRProd (Name id,raw_typ_of_id,acc))
-		   pat_ids
-		   (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
-	    )
-	    patl
-	    types
-	in
-	(* Checking if we can be in this branch 
-	   (will be used in the following recursive calls)
-	*)	   
-	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
-	(* 
-	   we first compute the other branch result (in ordrer to keep the order of the matching 
-	   as much as possible)
-	*)
-	let brl'_res =
-	  build_entry_lc_from_case_term
-	    env 
-	    types
-	    funname
-	    make_discr
-	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
-	    brl'
-	    avoid
-	    matched_expr
-	in
-	(* We now create the precondition of this branch i.e.
-
-	   1- the list of variable appearing in the different patterns of this branch and 
-	      the list of equation stating than el = patl (List.flatten ...)
-	   2- If there exists a previous branch which pattern unify with the one of this branch 
-              then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
-	*)
-      	let those_pattern_preconds =
-	  (List.flatten
-	    (
-	      list_map3
-	      (fun pat e typ_as_constr ->
-		 let this_pat_ids = ids_of_pat pat in 
-		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr 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),
-		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in 
-		      let raw_typ_of_id = 
-			Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
-		      in
-		      raw_typ_of_id
-			   )::acc
-		      else acc
-			
-		   )
-		   idl
-		   [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
-	      )
-	      patl
-	      matched_expr.value
-	      types
-	  )
-	  )
-	  @
-	  (if List.exists (function (unifl,_) ->
-			     let (unif,_) = 
-			       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 
-	     let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
-	     [(Prod Anonymous,make_discr pats_as_constr i  )]
-	   else 
-	     []
-	  )
-	in
-	(* We compute the result of the value returned by the branch*)
-	let return_res = build_entry_lc new_env funname new_avoid return in
-	(* and combine it with the preconds computed for this branch *)
-	let this_branch_res =
-	  List.map
-	    (fun res  ->
-	       { context = matched_expr.context@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 
-
-(* 
-   The second phase which reconstruct the real type of the constructor. 
-   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,k,t,b) -> 
-	let not_free_in_t id = not (is_free_in id t) in 
-	let new_crossed_types = t::crossed_types in 
-	begin
-	  match t with 
-	    | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id ->
-		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 
-			(*i The next call to mk_rel_id is valid since we are constructing the graph
-			  Ensures by: obvious
-			  i*) 
-
-			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  && n = Anonymous
-		  -> 
-		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
-		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities 
-		     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,k,t,b) ->
-	begin
-	  let not_free_in_t id = not (is_free_in id t) in
-	  let new_crossed_types = t :: crossed_types in
-	  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,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
-	    | _ -> anomaly "Should not have an anonymous function here" 
-		(* We have renamed all the anonymous functions during alpha_renaming phase *)
-	  
-	end
-    | RLetIn(_,n,t,b) -> 
-	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
-
-
-(* debuging wrapper *)
-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
-
-
-(* naive implementation of parameter detection. 
-
-   A parameter is an argument which is only preceded by parameters and whose 
-   calls are all syntaxically equal. 
-
-   TODO: Find a valid way to deal with implicit arguments here! 
-*)
-let rec compute_cst_params relnames params = function 
-  | RRef _ | RVar _ | REvar _ | RPatVar _ -> params
-  | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
-      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
-
-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,RType None))
-
-
-let do_build_inductive 
-    funnames (funsargs: (Names.name * rawconstr * bool) list list)  
-    returned_types 
-    (rtl:rawconstr list) =
-  let _time1 = System.get_time () in
-(*   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
-  (* alpha_renaming of the body to prevent variable capture during manipulation *)
-  let rtl_alpha = List.map (function rt ->  expand_as (alpha_rt [] rt)) rtl in
-  let rta = Array.of_list rtl_alpha in
-  (*i The next call to mk_rel_id is valid since we are constructing the graph
-    Ensures by: obvious
-    i*) 
-  let relnames = Array.map mk_rel_id funnames in
-  let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in 
-  (* Construction of the pseudo constructors *)
-  let env = 
-    Array.fold_right 
-      (fun id env -> 
-	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id))  env
-      )
-      funnames 
-      (Global.env ())
-  in      
-  let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in 
-  (* and of the real constructors*)
-  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 
-	 (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
-	 fst (
-	   rebuild_cons nb_args relnames.(i)
-	     []
-	     []
-	     rt 
-	 )
-      ) 
-      res.result 
-  in 
-  (* adding names to constructors  *)
- let next_constructor_id = ref (-1) in 
-  let mk_constructor_id i = 
-    incr next_constructor_id;
-    (*i The next call to mk_rel_id is valid since we are constructing the graph
-      Ensures by: obvious
-      i*) 
-    id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
-  in
-  let rel_constructors i rt : (identifier*rawconstr) list = 
-    next_constructor_id := (-1);
-    List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
-  in
-  let rel_constructors = Array.mapi rel_constructors resa in
-  (* Computing the set of parameters if asked *)
-  let rels_params = compute_params_name relnames_as_set funsargs  rel_constructors in
-  let nrel_params = List.length rels_params in
-  let rel_constructors = (* Taking into account the parameters in constructors *)
-    Array.map (List.map 
-    (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
-    rel_constructors
-  in
-  let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    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)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
-	    acc
-	   )
-      )
-      rel_first_args
-      (rebuild_return_type returned_types.(i))
-  in
-  (* We need to lift back our work topconstr but only with all information 
-     We mimick a Set Printing All. 
-     Then save the graphs and reset Printing options to their primitive values 
-  *)
-  let rel_arities = Array.mapi rel_arity funsargs in
-  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)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t)
-      )
-      rels_params
-  in 
-  let ext_rels_constructors = 
-    Array.map (List.map 
-      (fun (id,t) -> 
-	 false,((dummy_loc,id),
-		Flags.with_option
-		  Flags.raw_print
-		  (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
-	       )
-      ))
-      (rel_constructors)
-  in
-  let rel_ind i ext_rel_constructors = 
-    ((dummy_loc,relnames.(i)),
-    rel_params,
-    Some rel_arities.(i),
-    ext_rel_constructors),None
-  in
-  let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
-  let rel_inds = Array.to_list ext_rel_constructors in 
-(*   let _ =  *)
-(*   Pp.msgnl  (\* 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 () ++ str ":=" ++ *)
-(* 	     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 _time2 = System.get_time () in 
-  try 
-    with_full_print (Flags.silently (Command.build_mutual rel_inds)) true
-  with 
-    | UserError(s,msg) as e ->
-	let _time3 = System.get_time () in
-(* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
-	                  rel_inds
-	in
-	let msg = 		     
-	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,repacked_rel_inds))
-	    ++ fnl () ++
-	    msg
-	in
-	observe (msg);
-	raise e
-    | e -> 
-	let _time3 = System.get_time () in
-(* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
-	                  rel_inds
-	in
-	let msg = 		     
-	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,repacked_rel_inds)) 
-	    ++ fnl () ++
-	    Cerrors.explain_exn e
-	in
- 	observe msg;
-	raise e
-
-
-
-let build_inductive funnames funsargs returned_types rtl = 
-  try 
-    do_build_inductive funnames funsargs returned_types rtl
-  with e -> raise (Building_graph e)
-      
-