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.mli | |
| 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.mli')
| -rw-r--r-- | kernel/reduction.mli | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 88e6e70259..d34a0d99d3 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -142,6 +142,13 @@ val reduction_of_redexp : red_expr -> 'a reduction_function (*s Conversion Functions (uses closures, lazy strategy) *) +type conv_pb = + | CONV + | CONV_LEQ + +val pb_is_equal : conv_pb -> bool +val pb_equal : conv_pb -> conv_pb + type conversion_result = | Convertible of universes | NotConvertible @@ -161,20 +168,15 @@ type 'a conversion_function = val fconv : conv_pb -> 'a conversion_function -(* fconv has 4 instances: +(* fconv has 2 instances: \begin{itemize} \item [conv = fconv CONV] : conversion test, and adjust universes constraints - \item [conv_x = fconv CONV_X] : idem, without adjusting univ - (used in tactics) \item [conv_leq = fconv CONV_LEQ] : cumulativity test, adjust universes - \item [conv_x_leq = fconv CONV_X_LEQ] : idem, without adjusting - (used in tactics) \end{itemize} *) + val conv : 'a conversion_function val conv_leq : 'a conversion_function -val conv_x : 'a conversion_function -val conv_x_leq : 'a conversion_function (*s Obsolete Reduction Functions *) |