5
val generate_functional_principle :
6
(* do we accept interactive proving *)
8
(* induction principle on rel *)
12
(* Name of the new principle *)
13
(identifier) option ->
14
(* the compute functions to use *)
16
(* We prove the nth- principle *)
18
(* The tactic to use to make the proof w.r
21
(constr array -> int -> Tacmach.tactic) ->
24
val compute_new_princ_type_from_rel : constr array -> sorts array ->
28
exception No_graph_found
30
val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list
32
val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list -> unit
33
val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort) -> unit