Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 752 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
deleted file mode 100644
index b6b2cbd1..00000000
--- a/contrib/funind/indfun.ml
+++ /dev/null
@@ -1,752 +0,0 @@
-open Util
-open Names
-open Term
-open Pp
-open Indfun_common
-open Libnames
-open Rawterm
-open Declarations
-
-let is_rec_info scheme_info = 
-  let test_branche min acc (_,_,br) = 
-    acc || (
-      let new_branche = 
-	Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in 
-      let free_rels_in_br = Termops.free_rels new_branche in 
-      let max = min + scheme_info.Tactics.npredicates in 
-      Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
-    )
-  in
-  Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
-
-
-let choose_dest_or_ind scheme_info =
-    if is_rec_info scheme_info
-    then Tactics.new_induct false
-    else Tactics.new_destruct false
-
-
-let functional_induction with_clean c princl pat =
-  let f,args = decompose_app c in 
-  fun g ->      
-    let princ,bindings, princ_type = 
-      match princl with 
-	| None -> (* No principle is given let's find the good one *)
-	    begin
-	      match kind_of_term f with
-		| Const c' ->
-		    let princ_option = 
-		      let finfo = (* we first try to find out a graph on f *)
-			try find_Function_infos c' 
-			with Not_found -> 
-			  errorlabstrm "" (str "Cannot find induction information on "++
-					     Printer.pr_lconstr (mkConst c') )
-		      in
-		      match Tacticals.elimination_sort_of_goal g with 
-			| InProp -> finfo.prop_lemma
-			| InSet -> finfo.rec_lemma
-			| InType -> finfo.rect_lemma
-		    in
-		    let princ =  (* then we get the principle *)
-		      try mkConst (Option.get princ_option )
-		      with Option.IsNone -> 
-			(*i If there is not default lemma defined then, 
-			  we cross our finger and try to find a lemma named f_ind 
-			  (or f_rec, f_rect) i*)
-			let princ_name = 
-			  Indrec.make_elimination_ident
-			    (id_of_label (con_label c'))
-			    (Tacticals.elimination_sort_of_goal g)
-			in
-			try 
-			  mkConst(const_of_id princ_name )
-			with Not_found -> (* This one is neither defined ! *)
-			  errorlabstrm "" (str "Cannot find induction principle for "
-					   ++Printer.pr_lconstr (mkConst c') )
-		    in
-		    (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ)
-		| _ -> raise (UserError("",str "functional induction must be used with a function" ))
-		    
-	    end
-	| Some ((princ,binding)) -> 
-	    princ,binding,Tacmach.pf_type_of g princ
-    in
-    let princ_infos = Tactics.compute_elim_sig princ_type in 
-    let args_as_induction_constr =
-      let c_list = 
-	if princ_infos.Tactics.farg_in_concl 
-	then [c] else [] 
-      in
-      List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) 
-    in 
-    let princ' = Some (princ,bindings) in 
-    let princ_vars = 
-      List.fold_right 
-	(fun a acc -> 
-	  try Idset.add (destVar a) acc
-	  with _ -> acc
-	)
-	args
-	Idset.empty
-    in
-    let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in 
-    let old_idl = Idset.diff old_idl princ_vars in 
-    let subst_and_reduce g = 
-      if with_clean 
-      then
-	let idl = 
-	  map_succeed 
-	    (fun id -> 
-	       if Idset.mem id old_idl then failwith "subst_and_reduce";
-	       id 
-	    )
-	    (Tacmach.pf_ids_of_hyps g)
-	in 
-	let flag = 
-	  Rawterm.Cbv
-	    {Rawterm.all_flags 
-	     with Rawterm.rDelta = false; 		 
-	    }
-	in
-	Tacticals.tclTHEN
-	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
-	  (Hiddentac.h_reduce flag Tacticals.allClauses)	
-	  g
-      else Tacticals.tclIDTAC g 
-	
-    in
-    Tacticals.tclTHEN
-      (choose_dest_or_ind 
-	 princ_infos
-	 args_as_induction_constr
-	 princ'
-	 (None,pat)
-         None)
-      subst_and_reduce
-      g
-      
-      
-
-
-type annot = 
-    Struct of identifier 
-  | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
-  | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
-
-
-type newfixpoint_expr =
-    identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr
-
-let rec abstract_rawconstr c = function
-  | [] -> c
-  | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
-  | Topconstr.LocalRawAssum (idl,k,t)::bl ->
-      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
-        (abstract_rawconstr c bl)
-
-let interp_casted_constr_with_implicits sigma env impls c  =
-(*   Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
-  Constrintern.intern_gen false sigma env ~impls:([],impls) 
-    ~allow_patvar:false  ~ltacvars:([],[]) c
-
-
-(* 
-   Construct a fixpoint as a Rawterm 
-   and not as a constr
-*)
-let build_newrecursive
-(lnameargsardef)  =
-  let env0 = Global.env()
-  and sigma = Evd.empty
-  in
-  let (rec_sign,rec_impls) =
-    List.fold_left
-      (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
-        let arityc = Command.generalize_constr_expr arityc bl in
-        let arity = Constrintern.interp_type sigma env0 arityc in
-	let impl =
-	  if Impargs.is_implicit_args()
-	  then Impargs.compute_implicits  env0 arity
-	  else [] in
-	let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
-        (Environ.push_named (recname,None,arity) env, impls'))
-      (env0,[]) lnameargsardef in
-  let recdef =
-    (* Declare local notations *)
-    let fs = States.freeze() in
-    let def =
-      try
-	List.map
-	  (fun (_,_,bl,_,def)  ->
-             let def = abstract_rawconstr def bl in
-             interp_casted_constr_with_implicits
-	       sigma rec_sign rec_impls def
-	  )
-          lnameargsardef
-	with e ->
-	States.unfreeze fs; raise e in
-    States.unfreeze fs; def
-  in
-  recdef,rec_impls
-	
-
-let compute_annot (name,annot,args,types,body) =
-  let names = List.map snd (Topconstr.names_of_local_assums args) in
-  match annot with
-    | None ->
-        if List.length names > 1 then
-          user_err_loc
-            (dummy_loc,"Function",
-             Pp.str "the recursive argument needs to be specified");
-        let new_annot = (id_of_name (List.hd names)) in
-	(name,Struct new_annot,args,types,body)
-    | Some r -> (name,r,args,types,body)
-
-
-(* Checks whether or not the mutual bloc is recursive *) 
-let rec is_rec names = 
-  let names = List.fold_right Idset.add names Idset.empty in 
-  let check_id id names =  Idset.mem id names in 
-  let rec lookup names = function 
-    | RVar(_,id) -> check_id id names
-    | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
-    | RCast(_,b,_) -> lookup names b
-    | RRec _ -> error "RRec not handled"
-    | RIf(_,b,_,lhs,rhs) -> 
-	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  -> 
-	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
-    | RLetTuple(_,nal,_,t,b) -> lookup names t || 
-	lookup 
-	  (List.fold_left 
-	     (fun acc na -> Nameops.name_fold Idset.remove na acc)
-	     names
-	     nal
-	  )
-	  b
-    | RApp(_,f,args) -> List.exists (lookup names) (f::args)
-    | RCases(_,_,_,el,brl) -> 
-	List.exists (fun (e,_) -> lookup names e) el ||
-	  List.exists (lookup_br names) brl
-  and lookup_br names (_,idl,_,rt) = 
-    let new_names = List.fold_right Idset.remove idl names in 
-    lookup new_names rt
-  in
-  lookup names
-
-let prepare_body (name,annot,args,types,body) rt = 
-  let n = (Topconstr.local_binders_length args) in 
-(*   Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *)
-  let fun_args,rt' = chop_rlambda_n n rt in
-  (fun_args,rt')
-
-
-let derive_inversion fix_names =
-  try 
-    (* we first transform the fix_names identifier into their corresponding constant *)
-    let fix_names_as_constant = 
-      List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names 
-    in 
-    (* 
-       Then we check that the graphs have been defined 
-       If one of the graphs haven't been defined 
-       we do nothing
-    *)
-    List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
-    try
-      Invfun.derive_correctness 
-	Functional_principles_types.make_scheme
-	functional_induction 
-	fix_names_as_constant
-	(*i The next call to mk_rel_id is valid since we have just construct the graph 
-	  Ensures by : register_built
-	  i*) 
-	(List.map
-	   (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
-	   fix_names
-	)
-    with e -> 
-      msg_warning 
-	(str "Cannot built inversion information" ++ 
-	   if do_observe () then Cerrors.explain_exn e else mt ())
-  with _ -> ()
-
-let warning_error names e = 
-  match e with 
-    | Building_graph e -> 
-	Pp.msg_warning 
-	  (str "Cannot define graph(s) for " ++ 
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
-    | Defining_principle e -> 
-	Pp.msg_warning
-	  (str "Cannot define principle(s) for "++ 
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     if do_observe () then Cerrors.explain_exn e else mt ())
-    | _ -> anomaly ""
-
-let error_error names e = 
-  match e with 
-    | Building_graph e -> 
-	errorlabstrm ""  
-	  (str "Cannot define graph(s) for " ++ 
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
-    | _ -> anomaly ""
-
-let generate_principle  on_error
-    is_general do_built fix_rec_l recdefs  interactive_proof 
-    (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
-      Tacmach.tactic) : unit =
-  let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in
-  let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
-  let funs_args = List.map fst fun_bodies in
-  let funs_types =  List.map (function (_,_,_,types,_) -> types) fix_rec_l in
-  try 
-    (* We then register the Inductive graphs of the functions  *)
-    Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
-    if do_built 
-    then
-      begin
-	(*i The next call to mk_rel_id is valid since we have just construct the graph 
-	   Ensures by : do_built
-	i*) 
-	let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
-	let ind_kn =
-	  fst (locate_with_msg
-		 (pr_reference f_R_mut++str ": Not an inductive type!")
-		 locate_ind
-		 f_R_mut)
-	in
-	let fname_kn (fname,_,_,_,_) =
-	  let f_ref = Ident fname in
-	  locate_with_msg
-	    (pr_reference f_ref++str ": Not an inductive type!")
-	    locate_constant
-	    f_ref
-	in
-	let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in 
-	let _ = 
-	  list_map_i
-	    (fun i x ->
-	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in 
-	       let princ_type = Typeops.type_of_constant (Global.env()) princ
-	       in
-	       Functional_principles_types.generate_functional_principle
-		 interactive_proof 
-		 princ_type
-		 None
-		 None 
-		 funs_kn
-		 i
-		 (continue_proof  0 [|funs_kn.(i)|]) 
-	    )
-	    0
-	    fix_rec_l
-	in 
-	Array.iter (add_Function is_general) funs_kn;
-	()
-      end
-  with e -> 
-    on_error names e 
-
-let register_struct is_rec fixpoint_exprl = 
-  match fixpoint_exprl with 
-    | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> 
-	Command.declare_definition
-	  fname
-	  (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
-	  bl
-	  None
-  	  body
-	  (Some ret_type)
-	  (fun _ _ -> ())
-    | _ -> 
-	Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
-
-let generate_correction_proof_wf f_ref tcc_lemma_ref   
-    is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-    (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = 
-  Functional_principles_proofs.prove_principle_for_gen
-    (f_ref,functional_ref,eq_ref)
-    tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
-
-
-let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
-    pre_hook 
-    =  
-  let type_of_f = Command.generalize_constr_expr ret_type args in 
-  let rec_arg_num = 
-    let names = 
-      List.map
-	snd
-	(Topconstr.names_of_local_assums args) 
-    in 
-    match wf_arg with 
-      | None -> 
-	  if List.length names = 1 then 1
-	  else error "Recursive argument must be specified"
-      | Some wf_arg -> 
-	  list_index (Name wf_arg) names 
-  in
-  let unbounded_eq = 
-    let f_app_args = 
-      Topconstr.CAppExpl 
-	(dummy_loc, 
-	 (None,(Ident (dummy_loc,fname))) ,
-	 (List.map 
-	    (function
-	       | _,Anonymous -> assert false 
-	       | _,Name e -> (Topconstr.mkIdentC e)
-	    ) 
-	    (Topconstr.names_of_local_assums args)
-	 )
-	) 
-    in
-    Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
-		    [(f_app_args,None);(body,None)])
-  in
-  let eq = Command.generalize_constr_expr unbounded_eq args in 
-  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
-      nb_args relation =
-    try 
-      pre_hook 
-	(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
-	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-	);
-      derive_inversion [fname]
-    with e -> 
-      (* No proof done *) 
-      ()
-  in 
-  Recdef.recursive_definition 
-    is_mes fname rec_impls
-    type_of_f
-    wf_rel_expr
-    rec_arg_num
-    eq
-    hook
-    using_lemmas
-
-    
-let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = 
-  let wf_arg_type,wf_arg = 
-    match wf_arg with 
-      | None -> 
-	  begin
-	    match args with 
-	      | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x 
-	      | _ -> error "Recursive argument must be specified" 
-	  end
-      | Some wf_args -> 
-	  try 
-	    match 
-	      List.find 
-		(function 
-		   | Topconstr.LocalRawAssum(l,k,t) -> 
-		       List.exists 
-			 (function (_,Name id) -> id =  wf_args | _ -> false) 
-			 l 
-		   | _ -> false
-		)
-		args 
-	    with 
-	      | Topconstr.LocalRawAssum(_,k,t)  ->	    t,wf_args
-	      | _ -> assert false 
-	  with Not_found -> assert false 
-  in
-  let ltof = 
-    let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in 
-    Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp 
-      (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
-  in
-  let fun_from_mes = 
-    let applied_mes = 
-      Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg])    in
-    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) 
-  in
-  let wf_rel_from_mes = 
-    Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
-  in
-  register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) 
-    using_lemmas args ret_type body
-	  
-
-let do_generate_principle on_error register_built interactive_proof fixpoint_exprl  = 
-  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in 
-  let _is_struct = 
-    match fixpoint_exprl with 
-      | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
-	  let pre_hook = 
-	    generate_principle 
-	      on_error
-	      true
-	      register_built
-	      fixpoint_exprl 
-	      recdefs
-	      true
-	  in 
-	  if register_built 
-	  then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
-	  false
-      | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
-	  let pre_hook = 
-	    generate_principle 
-	      on_error
-	      true
-	      register_built
-	      fixpoint_exprl 
-	      recdefs
-	      true
-	  in 
-	  if register_built 
-	  then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
-	  true
-      | _ -> 
-	  let fix_names = 
-	    List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl 
-	  in
-	  let is_one_rec = is_rec fix_names  in
-	  let old_fixpoint_exprl =  
-	    List.map
-	      (function
-		 | (name,Some (Struct id),args,types,body),_ -> 
-		     let annot = 
-		       try Some (dummy_loc, id), Topconstr.CStructRec 
-		       with Not_found -> 
-			 raise (UserError("",str "Cannot find argument " ++ 
-					    Ppconstr.pr_id id)) 
-		     in 
- 		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
-		 | (name,None,args,types,body),recdef -> 
-		     let names =  (Topconstr.names_of_local_assums args) in
-		     if  is_one_rec recdef  && List.length names > 1 then
-		       user_err_loc
-			 (dummy_loc,"Function",
-			  Pp.str "the recursive argument needs to be specified in Function")
-		     else 
-		       let loc, na = List.hd names in
-			 (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
-		     (None:Vernacexpr.decl_notation)
-		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
-		     error 
-		       ("Cannot use mutual definition with well-founded recursion or measure")
-	      ) 
-	      (List.combine fixpoint_exprl recdefs)
-	  in
-	  (* ok all the expressions are structural *) 
-	  let fix_names = 
-	    List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl 
-	  in
-	  let is_rec = List.exists (is_rec fix_names) recdefs in
-	  if register_built then register_struct is_rec old_fixpoint_exprl;
-	  generate_principle
-	    on_error
-	    false
-	    register_built
-	    fixpoint_exprl
-	    recdefs 
-	    interactive_proof
-	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
-	  if register_built then derive_inversion fix_names;
-	  true;
-  in
-  ()
-
-open Topconstr
-let rec add_args id new_args b = 
-  match b with 
-  | CRef r -> 
-      begin      match r with 
-	| Libnames.Ident(loc,fname) when fname = id -> 
-	    CAppExpl(dummy_loc,(None,r),new_args)
-	| _ -> b
-      end
-  | CFix  _  | CCoFix _ -> anomaly "add_args : todo"
-  | CArrow(loc,b1,b2) -> 
-      CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
-  | CProdN(loc,nal,b1) -> 
-      CProdN(loc,
-	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, 
-	     add_args id new_args  b1)
-  | CLambdaN(loc,nal,b1) -> 
-      CLambdaN(loc,
-	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal, 
-	       add_args id new_args  b1)
-  | CLetIn(loc,na,b1,b2) -> 
-      CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
-  | CAppExpl(loc,(pf,r),exprl) -> 
-      begin 
-	match r with 
-	| Libnames.Ident(loc,fname) when fname = id -> 
-	    CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
-	| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
-      end
-  | CApp(loc,(pf,b),bl) -> 
-      CApp(loc,(pf,add_args id new_args b), 
-	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
-  | CCases(loc,sty,b_option,cel,cal) -> 
-      CCases(loc,sty,Option.map (add_args id new_args) b_option,
-	     List.map (fun (b,(na,b_option)) -> 
-			 add_args id new_args b,
-			 (na,Option.map (add_args id new_args) b_option)) cel, 
-	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
-	    )
-  | CLetTuple(loc,nal,(na,b_option),b1,b2) -> 
-      CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
-		add_args id new_args b1,
-		add_args id new_args b2
-	       )
-		
-  | CIf(loc,b1,(na,b_option),b2,b3) -> 
-      CIf(loc,add_args id new_args b1, 
-	  (na,Option.map (add_args id new_args) b_option),
-	  add_args id new_args b2,
-	  add_args id new_args b3
-	 )
-  | CHole _ -> b
-  | CPatVar _ -> b
-  | CEvar _ -> b
-  | CSort _ -> b
-  | CCast(loc,b1,CastConv(ck,b2))  -> 
-      CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
-  | CCast(loc,b1,CastCoerce) ->
-      CCast(loc,add_args id new_args b1,CastCoerce)
-  | CRecord _ -> anomaly "add_args : CRecord"
-  | CNotation _ -> anomaly "add_args : CNotation"
-  | CGeneralization _ -> anomaly "add_args : CGeneralization"
-  | CPrim _ -> b
-  | CDelimiters _ -> anomaly "add_args : CDelimiters"
-  | CDynamic _ -> anomaly "add_args : CDynamic"
-exception Stop of  Topconstr.constr_expr
-
-
-(* [chop_n_arrow n t] chops the [n] first arrows in [t] 
-   Acts on Topconstr.constr_expr 
-*)
-let rec chop_n_arrow n t = 
-  if n <= 0 
-  then t (* If we have already removed all the arrows then return the type *)
-  else (* If not we check the form of [t] *) 
-    match t with 
-      | Topconstr.CArrow(_,_,t) ->  (* If we have an arrow, we discard it and recall [chop_n_arrow] *)
-	  chop_n_arrow (n-1) t
-      | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : 
-					     either we need to discard more than the number of arrows contained
-					     in this product declaration then we just recall [chop_n_arrow] on
-					     the remaining number of arrow to chop and [t'] we discard it and 
-					     recall [chop_n_arrow], either this product contains more arrows 
-					     than the number we need to chop and then we return the new type
-					  *)
-	  begin 
-	    try 
-	      let new_n =
-		let rec aux (n:int) = function 
-		    [] -> n
-		| (nal,k,t'')::nal_ta' -> 
-		    let nal_l = List.length nal in 
-		    if n >= nal_l
-		    then 
-		      aux (n - nal_l) nal_ta'
-		    else 
-		      let new_t' = 
-			Topconstr.CProdN(dummy_loc,
-					((snd (list_chop n nal)),k,t'')::nal_ta',t')
-		      in 
-		      raise (Stop new_t')
-		in
-		aux n nal_ta'
-	    in 
-	      chop_n_arrow new_n t'
-	    with Stop t -> t
-	  end
-      | _ -> anomaly "Not enough products"
-  
-
-let rec get_args b t : Topconstr.local_binder list * 
-    Topconstr.constr_expr * Topconstr.constr_expr = 
-  match b with 
-    | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
-	begin
-	  let n = 
-	    (List.fold_left (fun n (nal,_,_) -> 
-			       n+List.length nal) 0 nal_ta )
-	  in
-	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
-	  (List.map (fun (nal,k,ta) -> 
-		       (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' 
-	end
-    | _ -> [],b,t
-
-
-let make_graph (f_ref:global_reference) =
- let c,c_body = 
-      match f_ref with 
-	| ConstRef c -> 
-	    begin try c,Global.lookup_constant c 
-	    with Not_found -> 
-	      raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
-	    end
-	| _ -> raise (UserError ("", str "Not a function reference") )
-
-  in
-  match c_body.const_body with
-    | None -> error "Cannot build a graph over an axiom !"
-    | Some b ->
-	let env = Global.env () in
-	let body = (force b) in
-	let extern_body,extern_type = 
-	  with_full_print 
-	    (fun () -> 
-	       (Constrextern.extern_constr false env body, 
-		Constrextern.extern_type false env
-                  (Typeops.type_of_constant_type env c_body.const_type)
-	       )
-	    )
-	    ()
-	in
-	let (nal_tas,b,t)  = get_args extern_body extern_type in
-	let expr_list = 
-	  match b with 
-	    | Topconstr.CFix(loc,l_id,fixexprl) -> 
-		let l = 
-		  List.map
-		    (fun (id,(n,recexp),bl,t,b) -> 
-		       let loc, rec_id = Option.get n in
-		       let new_args = 
-			 List.flatten 
-			   (List.map 
-			      (function
- 				 | Topconstr.LocalRawDef (na,_)-> []
-			      	 | Topconstr.LocalRawAssum (nal,_,_) -> 
-				     List.map 
-				       (fun (loc,n) -> 
-					  CRef(Libnames.Ident(loc, Nameops.out_name n))) 
-				       nal
-			      )
-			      nal_tas
-			   )
-		       in
-		       let b' = add_args (snd id) new_args b in 
-		       (id, Some (Struct rec_id),nal_tas@bl,t,b')
-		    )
-		    fixexprl
-		in
-		l
-	    | _ ->   
-		let id = id_of_label (con_label c) in 
-		[((dummy_loc,id),None,nal_tas,t,b)]
-	in
-	do_generate_principle error_error false false expr_list;
-	(* We register the infos *)
-	let mp,dp,_ = repr_con c in 
-	List.iter 
-	  (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) 
-	  expr_list
-
-
-(* let make_graph _ = assert false	 *)
-	  
-let do_generate_principle = do_generate_principle warning_error true 
-
-