X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_exportation%2FcicExportation.ml;h=e671effca9a565645d8d7f8c41f780d8b13f5d38;hb=0d3abcf9c11d95736820c9c6a8240d71f252941b;hp=c975ff11e8fb35ff92b192e698611f300af86431;hpb=616509324d3090e5c672c0452efea36f65b04975;p=helm.git diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml index c975ff11e..e671effca 100644 --- a/components/cic_exportation/cicExportation.ml +++ b/components/cic_exportation/cicExportation.ml @@ -294,6 +294,10 @@ let rec pp ~in_type t context = let rec aux argsno context = function Cic.Lambda (name,ty,bo) when argsno > 0 -> + let name = + match name with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name n -> Cic.Name (ppid n) in let args,res = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo