X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=e48e772079b86ef6d0d0eb8fafc9fca6706b3852;hb=0264ee034e3f485baf7070ad9b43cf69db94131b;hp=5e121ccfcb12c89595a051fe04758f1743203f9a;hpb=c83721701dbbd44d3d547fdec6c4a5658322f424;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 5e121ccfc..e48e77207 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -141,10 +141,8 @@ let match_coercion status ~metasenv ~subst ~context t =
  let db =
   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
  in
-  try
-   Some
-    (List.find
-      (fun (p,_,_) ->
+    (HExtlib.list_findopt
+      (fun (p,arity,cpos) _ ->
         try
          let t =
           match p,t with
@@ -155,10 +153,15 @@ let match_coercion status ~metasenv ~subst ~context t =
            | _,NCic.Appl (he::_) -> he
            | _,_ -> t
          in
-          NCicReduction.alpha_eq metasenv subst context p t
+         let b = NCicReduction.alpha_eq metasenv subst context p t in
+         if not b then None else
+         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
+         let pis = 
+           let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
+           aux ty
+         in
+         Some (p,pis - arity - cpos - 1,cpos)
         with
-         Failure _ -> false (* raised by split_nth *)
+         Failure _ -> None (* raised by split_nth *)
       ) db)
-  with
-   Not_found -> None
 ;;