aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/rules.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/rules.mli')
-rw-r--r--plugins/firstorder/rules.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index b804c93ae3..fc32621ca7 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -49,6 +49,6 @@ val forall_tac : seqtac with_backtracking
val left_exists_tac : inductive -> lseqtac with_backtracking
-val ll_forall_tac : types -> lseqtac with_backtracking
+val ll_forall_tac : types -> lseqtac with_backtracking
val normalize_evaluables : tactic