diff options
| author | soubiran | 2008-10-15 15:07:10 +0000 |
|---|---|---|
| committer | soubiran | 2008-10-15 15:07:10 +0000 |
| commit | d1df4f36c4e304d6ed446d09b64d1b3bf34bac16 (patch) | |
| tree | 957ac29812b949cc7aee31e4dae187fec02b31d5 /contrib | |
| parent | e9d5db3172cd707288166d3bf31506881ff1c16e (diff) | |
Report des commits 11417 et 11437 de la v8.2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index e52571aadb..edfdfb13ea 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -165,10 +165,10 @@ let rec extract_sfb_spec env mp = function | (l,SFBmodtype mtb) :: msig -> let specs = extract_sfb_spec env mp msig in (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs - | (l,SFBalias(mp1,_))::msig -> + | (l,SFBalias(mp1,typ_opt,_))::msig -> extract_sfb_spec env mp ((l,SFBmodule {mod_expr = Some (SEBident mp1); - mod_type = None; + mod_type = typ_opt; mod_constraints = Univ.Constraint.empty; mod_alias = Mod_subst.empty_subst; mod_retroknowledge = []})::msig) @@ -183,7 +183,7 @@ and extract_seb_spec env truetype = function (match extract_with_type env cb with (* cb peut contenir des kn *) | None -> mtb'' | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) - | SEBwith(mtb',With_module_body(idl,mp,_))-> + | SEBwith(mtb',With_module_body(idl,mp,_,_))-> Visit.add_mp mp; MTwith(extract_seb_spec env truetype mtb', ML_With_module(idl,mp)) @@ -250,13 +250,13 @@ let rec extract_sfb env mp all = function if all || Visit.needed_mp mp then (l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms else ms - | (l,SFBalias (mp1,cst)) :: msb -> + | (l,SFBalias (mp1,typ_opt,cst)) :: msb -> let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodule (extract_module env mp true {mod_expr = Some (SEBident mp1); - mod_type = None; + mod_type = typ_opt; mod_constraints= Univ.Constraint.empty; mod_alias = empty_subst; mod_retroknowledge = []})) :: ms |