- R.are_convertible f cc w vv
- in
- let f xv vv xt = function
-(* inserting a missing "modus ponens" *)
- | B.Appl (y2, B.Appl (y1, B.GRef uri)) when U.eq uri I.imp ->
- b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt])
- | B.Appl (y1, B.GRef uri) when U.eq uri I.not ->
- b_type_of f g c (mk_gref I.mp [y1; B.GRef I.con; xv; xt])
- | tt -> R.ho_whd (h xv vv xt tt) c tt
+ R.are_convertible f c w vv
+(* inserting a missing "modus ponens" *)
+ | R.GRef (uri, vs) when U.eq uri I.imp ->
+ L.log O.specs level (L.items1 "Rechecking coerced term");
+ b_type_of f g c (mk_gref I.mp (vs @ [xv; xt]))
+ | R.GRef (uri, vs) when U.eq uri I.all ->
+ L.log O.specs level (L.items1 "Rechecking coerced term");
+ b_type_of f g c (mk_gref I.alle (vs @ [xv; xt]))
+ | _ ->
+ error1 "not a function" c xt