summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
9f580d9)
`f ??????? x ???? y z` has to be rendered as `x y z`
<-----> <-->
cpos stat
let db =
DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
in
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
try
let t =
match p,t with
| _,NCic.Appl (he::_) -> he
| _,_ -> t
in
| _,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)
- Failure _ -> false (* raised by split_nth *)
+ Failure _ -> None (* raised by split_nth *)
- with
- Not_found -> None