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

5 files changed, 7 insertions, 55 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index 18ec721100..92b603e9dd 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -425,7 +425,7 @@ ftp-install: prep-ftp-install
 
 # prep-ftp-install: $(FTPDIR)/V$(VERSION)
 prep-ftp-install: 
-	- $(SERVEREXEC) mkdir -m g+w $(FTPDIR)/V$(VERSION)
+	- $(SERVEREXEC) mkdir -p -m g+w $(FTPDIR)/V$(VERSION)
 
 final-ftp-install:
 	$(SERVEREXEC) "'(cd $(FTPDIR); rm -f current;ln -sf V$(VERSION) current)'"
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
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 1a18e56748..e8e8653c85 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -251,12 +251,12 @@ let build_id_coercion idf_opt source =
   in
   (* juste pour verification *)
   let _ = 
-    try 
-      Reductionops.conv_leq env Evd.empty
-	(Typing.type_of env Evd.empty val_f) typ_f
-    with _ -> 
+    if not
+      (Reductionops.is_conv_leq env Evd.empty
+	(Typing.type_of env Evd.empty val_f) typ_f)
+    then
       error ("cannot be defined as coercion - "^
-	     "maybe a bad number of arguments") 
+             "maybe a bad number of arguments") 
   in
   let idf =
     match idf_opt with