From 7326d3fd7ba13dcf815e11dcdde1bd81257bdfce Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 18 Nov 2004 17:31:41 +0000
Subject: When a reference to a constructor is met its inductive type must be
 closed. This commit fixes the bug that prevented extraction of Lyon/CIRCUITS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6328 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extract_env.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 8c75f2df5c..04a23919b5 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -62,7 +62,14 @@ let in_mp v mp = MPset.mem mp v.mp
 
 let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
 let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
-let visit_ref v r = v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) 
+let visit_ref v r =
+ let r =
+  (* if we meet a constructor we must export the inductive definition *)
+  match r with
+     ConstructRef (r,_) -> IndRef r
+   | _ -> r
+ in
+  v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) 
 
 exception Impossible
 
-- 
cgit v1.2.3