nasty change in the lexer/parser:

[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 a558d99cfe98200fad80997f097affca1eec43b4..95ce44b647deac698084b914e2d12a6dd50bfcad 100644 (file)
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -88,6 +88,7 @@ let nast_of_cic ~idref ~output_type ~subst ~context =
     | NCic.Implicit `Hole -> idref (Ast.UserInput)
     | NCic.Implicit _ -> idref (Ast.Implicit)
     | NCic.Prod (n,s,t) ->
+        let n = if n.[0] = '_' then "_" else n in
         let binder_kind = `Forall in
          idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ctx s)),
           k ((n,NCic.Decl s)::ctx) t))