diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
| commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
| tree | 905dbbafa65dd7bf02823318326be2ca389f833f /plugins/extraction/extract_env.ml | |
| parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff) | |
Dir_path --> DirPath
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 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 85b9bde71..e94644821 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 Dir_path.empty l in + let kn = make_con mp DirPath.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 Dir_path.empty l in + let mind = make_mind mp DirPath.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 Dir_path.empty) vl in + let vc = Array.map (make_con mp DirPath.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 Dir_path.empty l in + let c = make_con mp DirPath.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 Dir_path.empty l in + let mind = make_mind mp DirPath.empty l in let b = Visit.needed_ind mind in if all || b then let d = Dind (mind, extract_inductive env mind) in |