diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:11:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:11:52 +0000 |
commit | e826e86af53c1621659c185f8d2f6cd2d56f66a6 (patch) | |
tree | 8918b141811beb015de012caa1510df2ff6848a8 | |
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
-rw-r--r-- | plugins/extraction/extract_env.ml | 3 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 8 |
2 files changed, 6 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index bc9047c0a..6bdea0b6c 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 diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 3dbfa7c02..725a70559 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -537,7 +537,7 @@ let _ = declare_summary "Extraction Inline" (* Grammar entries. *) let extraction_inline b l = - let refs = List.map Nametab.global l in + let refs = List.map Smartlocate.global_with_alias l in List.iter (fun r -> match r with | ConstRef _ -> () @@ -618,7 +618,7 @@ let _ = declare_summary "Extraction Implicit" let extraction_implicit r l = check_inside_section (); - Lib.add_anonymous_leaf (implicit_extraction (Nametab.global r,l)) + Lib.add_anonymous_leaf (implicit_extraction (Smartlocate.global_with_alias r,l)) (*s Extraction Blacklist of filenames not to use while extracting *) @@ -767,7 +767,7 @@ let _ = declare_summary "ML extractions custom match" let extract_constant_inline inline r ids s = check_inside_section (); - let g = Nametab.global r in + let g = Smartlocate.global_with_alias r in match g with | ConstRef kn -> let env = Global.env () in @@ -785,7 +785,7 @@ let extract_constant_inline inline r ids s = let extract_inductive r s l optstr = check_inside_section (); - let g = Nametab.global r in + let g = Smartlocate.global_with_alias r in match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in |