diff options
| author | sacerdot | 2004-11-18 17:31:41 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-18 17:31:41 +0000 |
| commit | 7326d3fd7ba13dcf815e11dcdde1bd81257bdfce (patch) | |
| tree | 51ce5b6de6a63b3e16699e9014b961bf863437ea | |
| parent | 1694cc318a22b3b523c6ab645f3c51fcdeb1998b (diff) | |
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
| -rw-r--r-- | contrib/extraction/extract_env.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |