From 67d5f78ad9593d51846bd6a69fca27e9a4ef0e6d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2009 11:42:46 +0000 Subject: [PATCH] match_coercion gives back the saturations, not the arity: `f ??????? x ???? y z` has to be rendered as `x y z` <-----> <--> cpos stat --- .../components/ng_refiner/nCicCoercion.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) 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 ;; -- 2.39.2