X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=a558d99cfe98200fad80997f097affca1eec43b4;hb=6b3242efcd29ea188ef09b445985abb06c5fad3a;hp=be731ba924fa9c1a2df699b0973568a1d11018de;hpb=210f84d727280d71f3f4814441665e2f800c427b;p=helm.git diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index be731ba92..a558d99cf 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -64,7 +64,7 @@ let nast_of_cic ~idref ~output_type ~subst ~context = idref (Ast.Ident (name,None)) with Failure "nth" | Invalid_argument "List.nth" -> idref (Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None))) - | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s false r, None)) + | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s true r, None)) | NCic.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in k ctx (NCicSubstitution.subst_meta lc t)