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/vconv.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/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index a35d1d88e..96445f696 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -219,12 +219,12 @@ and conv_eq_vect vt1 vt2 cu = let vconv pb env t1 t2 = let cu = - try conv_eq pb t1 t2 Constraint.empty + try conv_eq pb t1 t2 empty_constraint with NotConvertible -> infos := create_clos_infos betaiotazeta env; let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in - let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in + let cu = conv_val pb (nb_rel env) v1 v2 empty_constraint in cu in cu |