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/term_typing.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/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ab3e78fbc5..f765dd77e9 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -33,7 +33,7 @@ let constrain_type env j cst1 = function let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in assert (t = tj.utj_val); - NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3 + NonPolymorphicType t, union_constraints (union_constraints cst1 cst2) cst3 let local_constrain_type env j cst1 = function | None -> @@ -42,7 +42,7 @@ let local_constrain_type env j cst1 = function let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in assert (t = tj.utj_val); - t, Constraint.union (Constraint.union cst1 cst2) cst3 + t, union_constraints (union_constraints cst1 cst2) cst3 let translate_local_def env (b,topt) = let (j,cst) = infer env b in |