X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FExtractionMain.v;h=5deaf3a1b37d73c31bb4cd1a97ad607fb0b16d8d;hb=cef6be4de10acb4593acd67c0baa254f261971a1;hp=6406f90f31489cc0a98fafc1c9edad9021d405d6;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;p=coq-hetmet.git

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 6406f90..5deaf3a 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -13,7 +13,6 @@ Require Import Preamble.
 Require Import General.
 
 Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
 
 Require Import HaskKinds.
 Require Import HaskLiteralsAndTyCons.