open Names
open Term


val generate_functional_principle : 
  (* do we accept interactive proving *)
  bool ->
  (* induction principle on rel *) 
  types ->
  (* *)
  sorts array option -> 
  (* Name of the new principle *) 
  (identifier) option -> 
  (* the compute functions to use   *)
  constant array -> 
  (* We prove the nth- principle *)
  int  ->
  (* The tactic to use to make the proof w.r
     the number of params
  *)
  (constr array -> int -> Tacmach.tactic) -> 
  unit

val compute_new_princ_type_from_rel : constr array -> sorts array -> 
  types -> types


exception No_graph_found

val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list

val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list ->  unit
val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort)  ->  unit

