diff options
| author | filliatr | 1999-08-23 09:14:48 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-23 09:14:48 +0000 |
| commit | a86e0c41f5e9932140574b316343c3dfd321703c (patch) | |
| tree | 568d5d18799db01c86b2aa263310a4f8a66eb331 /kernel/reduction.ml | |
| parent | cd9afd3c84949dff733ab59f3bf838bc5863b532 (diff) | |
- suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujours
ajustés
- déplacement du type pb_conv dans Reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@20 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index d02d95277e..06f973ff62 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -731,6 +731,16 @@ let whd_betadeltaiotaeta env x = applist(whd_betadeltaiotaeta_stack env x []) (* Conversion *) (********************************************************************) +type conv_pb = + | CONV + | CONV_LEQ + +let pb_is_equal pb = pb = CONV + +let pb_equal = function + | CONV_LEQ -> CONV + | CONV -> CONV + type conversion_result = | Convertible of universes | NotConvertible @@ -779,8 +789,7 @@ let sort_cmp pb s0 s1 = | (Type u1, Type u2) -> (match pb with | CONV -> convert_of_constraint (enforce_eq u1 u2) - | CONV_LEQ -> convert_of_constraint (enforce_geq u2 u1) - | _ -> fun g -> Convertible g) + | CONV_LEQ -> convert_of_constraint (enforce_geq u2 u1)) | (_, _) -> fun _ -> NotConvertible (* Conversion between [lft1]term1 and [lft2]term2 *) @@ -923,8 +932,6 @@ let fconv cv_pb env t1 t2 = let conv env term1 term2 = fconv CONV env term1 term2 let conv_leq env term1 term2 = fconv CONV_LEQ env term1 term2 -let conv_x env term1 term2 = fconv CONV_X env term1 term2 -let conv_x_leq env term1 term2 = fconv CONV_X_LEQ env term1 term2 (********************************************************************) |