diff options
Diffstat (limited to 'plugins/subtac/subtac_command.mli')
-rw-r--r-- | plugins/subtac/subtac_command.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli index 6f73bc942..6c0c4340f 100644 --- a/plugins/subtac/subtac_command.mli +++ b/plugins/subtac/subtac_command.mli @@ -47,7 +47,7 @@ val telescope : Term.types * (Names.name * Term.types option * Term.types) list * Term.constr -val build_wellfounded : +val build_wellfounded : Names.identifier * 'a * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr -> Topconstr.constr_expr -> |