The backward compatible management of aliases for NG is now fully completed.

[helm.git] / helm / software / components / ng_cic_content / nTermCicContent.ml

diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index be731ba924fa9c1a2df699b0973568a1d11018de..a558d99cfe98200fad80997f097affca1eec43b4 100644 (file)
--- 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)