type_of_aux subst' metasenv' context te ugraph1
in
let rec count_prods context ty =
- match CicReduction.whd context ty with
+ match CicReduction.whd context ~subst:subst'' ty with
| Cic.Prod (n,s,t) ->
1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
let rec aux t m s ug it = function
| 0 -> t,it,m,s,ug
| n ->
- match CicReduction.whd context it with
+ match CicReduction.whd context ~subst:s it with
| Cic.Prod (_,src,tgt) ->
let newmeta, metaty, s, m, ug =
type_of_aux s m context (Cic.Implicit None) ug
let s,m,ug =
fo_unif_subst s context m metaty src ug
in
-(* prerr_endline "saturo"; *)
let t =
match t with
| Cic.Appl l -> Cic.Appl (l @ [newmeta])
aux te' metasenv'' subst'' ugraph2 inferredty
(max 0 (inf_prods - exp_prods))
in
-(* prerr_endline ("ottengo: " ^ CicPp.ppterm te'); *)
let (te', ty'), subst''',metasenv''',ugraph3 =
coerce_to_something true localization_tbl te' inferredty ty'
subst'' metasenv'' context ugraph2
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (function (metasenv,last,c) ->
+ (fun (metasenv,last,c) _ ->
match c with
| c when not (CoercGraph.is_composite c) ->
debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
ugraph in
match
HExtlib.list_findopt
- (fun (he,hetype,subst,metasenv,ugraph) ->
+ (fun (he,hetype,subst,metasenv,ugraph) _ ->
(* {{{ *)debug_print (lazy ("Try fix: "^
CicMetaSubst.ppterm_in_context ~metasenv subst he context));
debug_print (lazy (" of type: "^