From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 15 Jul 2009 11:42:46 +0000 (+0000)
Subject: match_coercion gives back the saturations, not the arity:
X-Git-Tag: make_still_working~3681
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=67d5f78ad9593d51846bd6a69fca27e9a4ef0e6d;p=helm.git

match_coercion gives back the saturations, not the arity:
`f ??????? x ???? y z` has to be rendered as `x y z`
   <----->   <-->
    cpos     stat
---

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
 ;;