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/inductive.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/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 289968eb53..07195c493f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -294,7 +294,7 @@ let is_correct_arity env c pj ind specif params = let univ = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ) + srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ) | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) let ksort = match kind_of_term (whd_betadeltaiota env a2) with | Sort s -> family_of_sort s @@ -304,13 +304,13 @@ let is_correct_arity env c pj ind specif params = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in check_allowed_sort ksort specif; - Constraint.union u univ + union_constraints u univ | _, (_,Some _,_ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) in - try srec env pj.uj_type (List.rev arsign) Constraint.empty + try srec env pj.uj_type (List.rev arsign) empty_constraint with LocalArity kinds -> error_elim_arity env ind (elim_sorts specif) c pj kinds |