test de conversion laissait echapper exception NotConvertible

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 31 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