diff options
| author | letouzey | 2010-12-18 16:35:15 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-18 16:35:15 +0000 |
| commit | 2a451f1809389beb123985d746f2e8febd46832e (patch) | |
| tree | 0bedd2eb88e2ec865070b4757546a4ec4a7fbf6b /kernel/subtyping.ml | |
| parent | 1c98af511e3cdc84c97bfc615a4c012059539d4f (diff) | |
Univ.constraints made fully abstract instead of being a Set of abstract stuff
No need to tell the world about the fact that constraints are
implemented via caml's Set. Other modules just need to know about
the empty and union functions (and addition functions "enforce_geq"
and "enforce_eq" that were already there).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8e74ff7259..93844ce5bd 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -69,7 +69,7 @@ let make_label_map mp list = let check_conv_error error cst f env a1 a2 = try - Constraint.union cst (f env a1 a2) + union_constraints cst (f env a1 a2) with NotConvertible -> error () @@ -369,7 +369,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = if equiv then let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in - Univ.Constraint.union + Univ.union_constraints (check_signatures cst env mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 mtb1.typ_delta mtb2.typ_delta) @@ -413,7 +413,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = let check_subtypes env sup super = let env = add_module (module_body_of_type sup.typ_mp sup) env in - check_modtypes Constraint.empty env + check_modtypes empty_constraint env (strengthen env sup sup.typ_mp) super empty_subst (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false |