From 2a451f1809389beb123985d746f2e8febd46832e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 18 Dec 2010 16:35:15 +0000
Subject: 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
---
 kernel/term_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.ml')

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
-- 
cgit v1.2.3