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 5e121ccfcb12c89595a051fe04758f1743203f9a..e48e772079b86ef6d0d0eb8fafc9fca6706b3852 100644 (file)
--- 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
 ;;