]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.ml
- ported to latest CicAst.Ident format (Some [] <> None)
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml
index 7c8261faebc372e2c92772bd1e50f3da3fc1af7f..f530a31beb30906e3dbc8f450299c6b87c53bcb4 100644 (file)
@@ -112,9 +112,7 @@ EXTEND
         PAREN "]" ->
           substs
       ] ->
-        (match subst with
-        | Some l -> CicAst.Ident (s, l)
-        | None -> CicAst.Ident (s, []))
+        CicAst.Ident (s, subst)
     ]
   ];
   name: [ (* as substituted_name with no explicit substitution *)