diff options
| author | letouzey | 2011-05-05 15:11:52 +0000 |
|---|---|---|
| committer | letouzey | 2011-05-05 15:11:52 +0000 |
| commit | e826e86af53c1621659c185f8d2f6cd2d56f66a6 (patch) | |
| tree | 8918b141811beb015de012caa1510df2ff6848a8 /plugins/extraction/extract_env.ml | |
| parent | 909c945e02ecc07b15ab2f41595bb2ec2ad97abc (diff) | |
Extraction: allow extraction foo when foo is an alias notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14094 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index bc9047c0ab..6bdea0b6c9 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -506,7 +506,8 @@ let rec locate_ref = function | r::l -> let q = snd (qualid_of_reference r) in let mpo = try Some (Nametab.locate_module q) with Not_found -> None - and ro = try Some (Nametab.locate q) with Not_found -> None in + and ro = try Some (Smartlocate.global_with_alias r) with _ -> None + in match mpo, ro with | None, None -> Nametab.error_global_not_found q | None, Some r -> let refs,mps = locate_ref l in r::refs,mps |