aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/Vericertlib.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/common/Vericertlib.v')
-rw-r--r--src/common/Vericertlib.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index f2754be..b58ebd4 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -29,7 +29,6 @@ Require Import Coq.micromega.Lia.
Require Export compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
-Require Export vericert.common.VericertTactics.
Require Import vericert.common.Show.
(* Depend on CompCert for the basic library, as they declare and prove some