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/indtypes.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/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 383bdc2ef3..0798bf18ad 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -160,7 +160,7 @@ let inductive_levels arities inds = arity or type constructor; we do not to recompute universes constraints *) let constraint_list_union = - List.fold_left Constraint.union Constraint.empty + List.fold_left union_constraints empty_constraint let infer_constructor_packet env_ar_par params lc = (* type-check the constructors *) @@ -197,7 +197,7 @@ let typecheck_inductive env mie = full_arity is used as argument or subject to cast, an upper universe will be generated *) let full_arity = it_mkProd_or_LetIn arity.utj_val params in - let cst = Constraint.union cst cst2 in + let cst = union_constraints cst cst2 in let id = ind.mind_entry_typename in let env_ar' = push_rel (Name id, None, full_arity) @@ -226,7 +226,7 @@ let typecheck_inductive env mie = infer_constructor_packet env_ar_par params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in let ind' = (arity_data,consnames,info,lc',cstrs_univ) in - (ind'::inds, Constraint.union cst cst')) + (ind'::inds, union_constraints cst cst')) mie.mind_entry_inds arity_list ([],cst) in |