- 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

4 files changed, 20 insertions, 30 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
 
 
 (********************************************************************)
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 *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 2f7838b2d9..87cc1aaaec 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -61,8 +61,6 @@ type typed_term = typed_type judge
 
 let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
-type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
-
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
@@ -825,17 +823,6 @@ let sort_hdchar = function
   | Prop(_) -> "P"
   | Type(_) -> "T"
 
-let pb_is_univ_adjust pb =
-  pb = CONV or pb = CONV_LEQ
-
-let pb_is_equal pb =
-  pb = CONV or pb = CONV_X
-
-let pb_equal = function
-  | CONV_LEQ -> CONV
-  | CONV_X_LEQ -> CONV_X
-  | pb -> pb
-
 (* Level comparison for information extraction : Prop <= Type *)
 let le_kind l m = (isprop l) or (is_Type m)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index cca056228b..82c54f0bbf 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -58,9 +58,6 @@ type typed_term = typed_type judge
 
 val typed_app : (constr -> constr) -> typed_type -> typed_type
 
-type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
-
-
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
   manipulation of terms. Some of these functions may be overlapped with
@@ -473,9 +470,6 @@ val same_kind : constr -> constr -> bool
 val le_kind : constr -> constr -> bool
 val le_kind_implicit : constr -> constr -> bool
 
-val pb_is_univ_adjust : conv_pb -> bool
-val pb_is_equal : conv_pb -> bool
-val pb_equal : conv_pb -> conv_pb
 val sort_hdchar : sorts -> string