From 0a2738fe2e171cc6661824cd6525ee5d5c317334 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 7 Mar 2011 15:37:59 +0000
Subject: Extraction: a warning when an opaque constant is enterred

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13891 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/modutil.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction/modutil.ml')

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 21dfee666..027b24787 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -332,7 +332,9 @@ let rec depcheck_se = function
     let refs = declared_refs d in
     let refs' = List.filter is_needed refs in
     if refs' = [] then
-      (List.iter remove_info_axiom refs; se')
+      (List.iter remove_info_axiom refs;
+       List.iter remove_opaque refs;
+       se')
     else begin
       List.iter found_needed refs';
       (* Hack to avoid extracting unused part of a Dfix *)
-- 
cgit v1.2.3