in
R.are_convertible f c w vv
(* inserting a missing "modus ponens" *)
- | R.GRef (uri, vs) when U.eq uri I.imp ->
+ | R.GRef (uri, vs) when U.eq uri I.imp && !R.ext = R.No ->
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 ->
+ | R.GRef (uri, vs) when U.eq uri I.all && !R.ext = R.No ->
L.log O.specs level (L.items1 "Rechecking coerced term");
b_type_of f g c (mk_gref I.alle (vs @ [xt; xv]))
| _ ->
and type_of f g c x =
let f t u = L.unbox level; f t u in
L.box level; b_type_of f g c x
-