aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/logic.mli')
-rw-r--r--proofs/logic.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli
index a1c525a34..3c960b657 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -61,7 +61,7 @@ type refiner_error =
exception RefinerError of refiner_error
-val error_cannot_unify : path_kind -> constr * constr -> 'a
+val error_cannot_unify : constr * constr -> 'a
val catchable_exception : exn -> bool