From a86e0c41f5e9932140574b316343c3dfd321703c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 23 Aug 1999 09:14:48 +0000
Subject:  - 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
---
 kernel/reduction.mli | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'kernel/reduction.mli')

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 *)
-- 
cgit v1.2.3