aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/subtac_classes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_classes.mli')
-rw-r--r--plugins/subtac/subtac_classes.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index c7687abf3..5b5c02037 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -33,7 +33,7 @@ val new_instance :
?global:bool ->
local_binder list ->
typeclass_constraint ->
- constr_expr ->
+ constr_expr option ->
?generalize:bool ->
int option ->
identifier * Subtac_obligations.progress