summaryrefslogtreecommitdiff
path: root/kernel/subtyping.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /kernel/subtyping.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'kernel/subtyping.ml')
-rw-r--r--kernel/subtyping.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 14020c0b..98ee1dbb 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 11142 2008-06-18 15:37:31Z soubiran $ i*)
+(*i $Id: subtyping.ml 11453 2008-10-15 14:42:34Z soubiran $ i*)
(*i*)
open Util
@@ -33,7 +33,7 @@ type namedobject =
| IndConstr of constructor * mutual_inductive_body
| Module of module_body
| Modtype of module_type_body
- | Alias of module_path
+ | Alias of module_path * struct_expr_body option
(* adds above information about one mutual inductive: all types and
constructors *)
@@ -64,7 +64,7 @@ let make_label_map mp list =
add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
| SFBmodule mb -> add_map (Module mb)
| SFBmodtype mtb -> add_map (Modtype mtb)
- | SFBalias (mp,cst) -> add_map (Alias mp)
+ | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt))
in
List.fold_right add_one list Labmap.empty
@@ -352,23 +352,23 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
begin
match info1 with
| Module msb -> check_modules cst env msid1 l msb msb2 alias
- | Alias mp ->let msb =
+ | Alias (mp,typ_opt) ->let msb =
{mod_expr = Some (SEBident mp);
- mod_type = Some (eval_struct env (SEBident mp));
+ mod_type = typ_opt;
mod_constraints = Constraint.empty;
mod_alias = (lookup_modtype mp env).typ_alias;
mod_retroknowledge = []} in
check_modules cst env msid1 l msb msb2 alias
| _ -> error_not_match l spec2
end
- | SFBalias (mp,_) ->
+ | SFBalias (mp,typ_opt,_) ->
begin
match info1 with
- | Alias mp1 -> check_modpath_equiv env mp mp1; cst
+ | Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst
| Module msb ->
let msb1 =
{mod_expr = Some (SEBident mp);
- mod_type = Some (eval_struct env (SEBident mp));
+ mod_type = typ_opt;
mod_constraints = Constraint.empty;
mod_alias = (lookup_modtype mp env).typ_alias;
mod_retroknowledge = []} in