diff options
Diffstat (limited to 'contrib/funind/new_arg_principle.mli')
| -rw-r--r-- | contrib/funind/new_arg_principle.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli index ad71ebd05..cad68da67 100644 --- a/contrib/funind/new_arg_principle.mli +++ b/contrib/funind/new_arg_principle.mli @@ -31,3 +31,4 @@ val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array -> Term.types -> Term.types val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list -> unit +val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) -> unit |