Deprecate Evarconv.e_conv,e_cumul

1 files changed, 18 insertions, 14 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e8b17d694..ea8557b18 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -48,31 +48,35 @@ exception NoCoercion
 exception NoCoercionNoUnifier of evar_map * unification_error
 
 (* Here, funj is a coercion therefore already typed in global context *)
-let apply_coercion_args env evd check isproj argl funj =
-  let evdref = ref evd in
-  let rec apply_rec acc typ = function
+let apply_coercion_args env sigma check isproj argl funj =
+  let rec apply_rec sigma acc typ = function
     | [] ->
       if isproj then
-	let cst = fst (destConst !evdref (j_val funj)) in
+        let cst = fst (destConst sigma (j_val funj)) in
 	let p = Projection.make cst false in
 	let pb = lookup_projection p env in
 	let args = List.skipn pb.Declarations.proj_npars argl in
 	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
-	  { uj_val = applist (mkProj (p, hd), tl);
-	    uj_type = typ }
+        sigma, { uj_val = applist (mkProj (p, hd), tl);
+                 uj_type = typ }
       else
-	{ uj_val = applist (j_val funj,argl);
-	  uj_type = typ }
+        sigma, { uj_val = applist (j_val funj,argl);
+                 uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
-      match EConstr.kind !evdref (whd_all env !evdref typ) with
+      match EConstr.kind sigma (whd_all env sigma typ) with
       | Prod (_,c1,c2) ->
-        if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then
-	  raise NoCoercion;
-        apply_rec (h::acc) (subst1 h c2) restl
+        let sigma =
+          if check then
+            begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with
+              | None -> raise NoCoercion
+              | Some sigma -> sigma
+            end
+          else sigma
+        in
+        apply_rec sigma (h::acc) (subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args.")
   in
-  let res = apply_rec [] funj.uj_type argl in
-    !evdref, res
+  apply_rec sigma [] funj.uj_type argl
 
 (* appliquer le chemin de coercions de patterns p *)
 let apply_pattern_coercion ?loc pat p =