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 --- checker/environ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/environ.ml') diff --git a/checker/environ.ml b/checker/environ.ml index 8c23a7e46..d960e2a7c 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -98,7 +98,7 @@ let named_type id env = (* Universe constraints *) let add_constraints c env = - if c == Constraint.empty then + if c == empty_constraint then env else let s = env.env_stratification in -- cgit v1.2.3