Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about

backtracking on coercion classes when a coercion path fails).



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

1 files changed, 12 insertions, 19 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 4ff60b41f..85e14d482 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -78,10 +78,6 @@ module Default = struct
       | App (f,l) -> mkApp (whd_evar sigma f,l)
       | _ -> whd_evar sigma t
 
-  let class_of1 env evd t =
-    let sigma = evars_of evd in
-    class_of env sigma (whd_app_evar sigma t)
-
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
     let rec apply_rec acc typ = function
@@ -107,18 +103,16 @@ module Default = struct
 
   (* raise Not_found if no coercion found *)
   let inh_pattern_coerce_to loc pat ind1 ind2 =
-    let i1 = inductive_class_of ind1 in
-    let i2 = inductive_class_of ind2 in
-    let p = lookup_pattern_path_between (i1,i2) in
+    let p = lookup_pattern_path_between (ind1,ind2) in
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
-  let apply_coercion env p hj typ_cl =
+  let apply_coercion env sigma p hj typ_cl =
     try 
       fst (List.fold_left
              (fun (ja,typ_cl) i -> 
 		let fv,isid = coercion_value i in
-		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 		let jres = apply_coercion_args env argl fv in
 		  (if isid then 
 		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -137,16 +131,15 @@ module Default = struct
 	      (evd',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env evd j.uj_type in
-      	       let p = lookup_path_to_fun_from i1 in
-		 (evd,apply_coercion env p j t)
+      	       let t,p =
+		 lookup_path_to_fun_from env (evars_of evd) j.uj_type in
+		 (evd,apply_coercion env (evars_of evd) p j t)
 	     with Not_found -> (evd,j))
 
   let inh_tosort_force loc env evd j =
     try
-      let t,i1 = class_of1 env evd j.uj_type in
-      let p = lookup_path_to_sort_from i1 in
-      let j1 = apply_coercion env p j t in 
+      let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in
+      let j1 = apply_coercion env (evars_of evd) p j t in 
       let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
         (evd,type_judgment env j2)
     with Not_found ->
@@ -173,12 +166,12 @@ module Default = struct
     else
     let v', t' =
       try 
-	let t1,i1 = class_of1 env evd c1 in
-	let t2,i2 = class_of1 env evd t in
-	let p = lookup_path_between (i2,i1) in
+	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
 	  match v with
 	      Some v -> 
-		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		let j =
+		  apply_coercion env (evars_of evd) p
+		    {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
       with Not_found -> raise NoCoercion