aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/logic.mli')
-rw-r--r--proofs/logic.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ba1ca7031..dfe40228f 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -55,7 +55,6 @@ type refiner_error =
(*i Errors raised by the tactics i*)
| CannotUnify of constr * constr
| CannotGeneralize of constr
- | BadTacticArgs of string * tactic_arg list
| IntroNeedsProduct
| DoesNotOccurIn of constr * identifier