aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/subtac_command.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_command.mli')
-rw-r--r--plugins/subtac/subtac_command.mli2
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 ->