aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/subtac_classes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/subtac_classes.mli')
-rw-r--r--contrib/subtac/subtac_classes.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 583c1a165..917ed8059 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -34,9 +34,9 @@ val type_ctx_instance : Evd.evar_defs ref ->
val new_instance :
?global:bool ->
- Topconstr.local_binder list ->
+ local_binder list ->
typeclass_constraint ->
- binder_def_list ->
+ constr_expr ->
?generalize:bool ->
int option ->
identifier * Subtac_obligations.progress