3 files changed, 1 insertions, 49 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9b51abff3b..8ebc170df6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -453,9 +453,6 @@ let fakey = Profile.declare_profile "fhnf_apply";;
 let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
 *)
 
-type  conversion_function = 
-    env ->  evar_map -> constr -> constr -> constraints
-
 (* Conversion utility functions *)
 
 type conversion_test = constraints -> constraints
@@ -491,34 +488,6 @@ let base_sort_cmp pb s0 s1 =
     | (_, _) -> false
 
 
-let conv env sigma t1 t2 =
-  Reduction.conv env (nf_evar sigma t1) (nf_evar sigma t2)
-let conv_leq env sigma t1 t2 =
-  Reduction.conv env (nf_evar sigma t1) (nf_evar sigma t2)
-let fconv = function CONV -> conv | CUMUL -> conv_leq
-
-(*
-let convleqkey = Profile.declare_profile "conv_leq";;
-let conv_leq env sigma t1 t2 =
-  Profile.profile4 convleqkey conv_leq env sigma t1 t2;;
-
-let convkey = Profile.declare_profile "conv";;
-let conv env sigma t1 t2 =
-  Profile.profile4 convleqkey conv env sigma t1 t2;;
-*)
-
-let conv_forall2 f env sigma v1 v2 =
-  array_fold_left2 
-    (fun c x y -> let c' = f env sigma x y in Constraint.union c c')
-    Constraint.empty
-    v1 v2
-
-let conv_forall2_i f env sigma v1 v2 =
-  array_fold_left2_i 
-    (fun i c x y -> let c' = f i env sigma x y in Constraint.union c c')
-    Constraint.empty
-    v1 v2
-
 let test_conversion f env sigma x y =
   try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true
   with NotConvertible -> false
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d2f260b7b0..2a76441ad1 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -169,23 +169,6 @@ val pb_equal : conv_pb -> conv_pb
 val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
 val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
 
-type  conversion_function = 
-    env ->  evar_map -> constr -> constr -> constraints
-
-(* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
-   [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
-
-val conv :  conversion_function
-val conv_leq :  conversion_function
-
-val conv_forall2 : 
-   conversion_function -> env ->  evar_map -> constr array 
-    -> constr array -> constraints
-
-val conv_forall2_i : 
-  (int ->  conversion_function) -> env ->  evar_map
-    -> constr array -> constr array -> constraints
-
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
 val is_fconv : conv_pb -> env ->  evar_map -> constr -> constr -> bool
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fc4b50ed26..b41947d308 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -113,7 +113,7 @@ let rec execute mf env sigma cstr =
         let j1 = execute mf env sigma c1 in
         let j2 = execute mf env sigma c2 in
         let j2 = type_judgment env sigma j2 in
-        let _ = conv_leq env sigma j1.uj_type j2.utj_val in
+        let _ =  judge_of_cast env j1 j2 in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let j3 = execute mf env1 sigma c3 in
         judge_of_letin env name j1 j2 j3