diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-18 16:35:15 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-18 16:35:15 +0000 |
| commit | 2a451f1809389beb123985d746f2e8febd46832e (patch) | |
| tree | 0bedd2eb88e2ec865070b4757546a4ec4a7fbf6b /kernel/reduction.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/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cbcbd151e..c865c92bf 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -197,9 +197,9 @@ let sort_cmp pb s0 s1 cuniv = | (_, _) -> raise NotConvertible -let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty +let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint -let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty +let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint let rec no_arg_available = function | [] -> true @@ -426,10 +426,10 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv = let clos_fconv trans cv_pb evars env t1 t2 = let infos = trans, create_clos_infos ~evars betaiotazeta env in - ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty + ccnv cv_pb infos ELID ELID (inject t1) (inject t2) empty_constraint let trans_fconv reds cv_pb evars env t1 t2 = - if eq_constr t1 t2 then Constraint.empty + if eq_constr t1 t2 then empty_constraint else clos_fconv reds cv_pb evars env t1 t2 let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None) @@ -448,8 +448,8 @@ let conv_leq_vecti ?(evars=fun _->None) env v1 v2 = let c' = try conv_leq ~evars env t1 t2 with NotConvertible -> raise (NotConvertibleVect i) in - Constraint.union c c') - Constraint.empty + union_constraints c c') + empty_constraint v1 v2 |