+ | NCic.Appl args as t ->
+ let args =
+ if not !Acic2content.hide_coercions then args
+ else
+ match
+ NCicCoercion.match_coercion status ~metasenv ~context ~subst t
+ with
+ | None -> args
+ | Some (_,sats,cpos) ->
+(* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di
+ argomenti da saltare, come prima! *)
+ if cpos < List.length args - 1 then
+ List.nth args (cpos + 1) ::
+ try snd (HExtlib.split_nth (cpos+sats+2) args) with Failure _->[]
+ else
+ args
+ in
+ (match args with
+ [arg] -> idref (k ~context arg)
+ | _ -> idref (Ast.Appl (List.map (k ~context) args)))