diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:57:08 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:57:08 +0000 |
commit | f42dd8d8530e6227621ccd662741f1da23700304 (patch) | |
tree | 1838306cdafaa8486ec792c1ab48b64162e027c9 /plugins/extraction/extract_env.ml | |
parent | 67f5c70a480c95cfb819fc68439781b5e5e95794 (diff) |
Modulification of dir_path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/extract_env.ml')
-rw-r--r-- | plugins/extraction/extract_env.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3cd3f7f8a..754016715 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl = let rec extract_sfb_spec env mp = function | [] -> [] | (l,SFBconst cb) :: msig -> - let kn = make_con mp empty_dirpath l in + let kn = make_con mp Dir_path.empty l in let s = extract_constant_spec env kn cb in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let mind = make_mind mp empty_dirpath l in + let mind = make_mind mp Dir_path.empty l in let s = Sind (mind, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs @@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function | (l,SFBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vc = Array.map (make_con mp empty_dirpath) vl in + let vc = Array.map (make_con mp Dir_path.empty) vl in let ms = extract_sfb env mp all msb in let b = Array.exists Visit.needed_con vc in if all || b then @@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function else ms with Impossible -> let ms = extract_sfb env mp all msb in - let c = make_con mp empty_dirpath l in + let c = make_con mp Dir_path.empty l in let b = Visit.needed_con c in if all || b then let d = extract_constant env c cb in @@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function else ms) | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in - let mind = make_mind mp empty_dirpath l in + let mind = make_mind mp Dir_path.empty l in let b = Visit.needed_ind mind in if all || b then let d = Dind (mind, extract_inductive env mind) in |