aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Inclusion.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Inclusion.v')
-rw-r--r--lib/Inclusion.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
index 1df7517f..15e37c46 100644
--- a/lib/Inclusion.v
+++ b/lib/Inclusion.v
@@ -22,6 +22,7 @@ A second tactic, [incl_tac], handles goals of the form
*)
Require Import List.
+Require Import Bool.
Require Import ArithRing.
Ltac all_app e :=