diff options
| author | letouzey | 2001-11-12 13:33:49 +0000 |
|---|---|---|
| committer | letouzey | 2001-11-12 13:33:49 +0000 |
| commit | 2f611e10fb3dc42fc00d80b1e087fa33f6fc846e (patch) | |
| tree | b81fb765ed77fe2d944495e5313b651fede45757 /contrib/extraction/extract_env.ml | |
| parent | b731edadffd527a907a6aa4b5a420b6a8dbe4690 (diff) | |
suite du petit oups
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/extract_env.ml')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 6969c412a8..7b997d48cf 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -165,7 +165,11 @@ let extract_reference r = if is_ml_extraction r then print_user_extract r else - mSGNL (ToplevelPp.pp_decl (List.find (decl_in_r r) (local_optimize [r]))) + let d = list_last (local_optimize [r]) in + mSGNL (ToplevelPp.pp_decl + (if (decl_in_r r d) || d = Dtype([],true) || d = Dtype([],false) + then d + else List.find (decl_in_r r) (local_optimize [r]))) let _ = vinterp_add "Extraction" |