diff options
Diffstat (limited to 'contrib/funind/functional_principles_types.mli')
| -rw-r--r-- | contrib/funind/functional_principles_types.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli index cf28c6e6c..6fa4fa70c 100644 --- a/contrib/funind/functional_principles_types.mli +++ b/contrib/funind/functional_principles_types.mli @@ -21,8 +21,11 @@ val generate_functional_principle : (constr array -> int -> Tacmach.tactic) -> unit -val compute_new_princ_type_from_rel : constr array -> sorts array -> - types -> types +(* TODO: hide [rel_to_fun_info] and [compute_new_princ_type_from_rel]. *) +type rel_to_fun_info = { thefun:constr; theargs: int array } + +val compute_new_princ_type_from_rel : (rel_to_fun_info list) Indfun_common.Link.t + -> sorts array -> types -> types exception No_graph_found |