From 54b96940073aa1506dd6d4ed0fe8277c6360ef54 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 3 Dec 2018 11:04:20 +0100
Subject: Remove leftover code that used to handle ml4 files.

---
 lib/coqProject_file.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'lib/coqProject_file.mli')

diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 20b276ce8c..39c5d019d0 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -22,7 +22,6 @@ type project = {
 
   v_files : string sourced list;
   mli_files : string sourced list;
-  ml4_files : string sourced list;
   mlg_files : string sourced list;
   ml_files : string sourced list;
   mllib_files : string sourced list;
-- 
cgit v1.2.3