1. bug fixed: Unicode characters that are not mapped to TeX macros used to

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 088d1b69d690562e4ce74281f3109cccdee259d0..69ae68aeec37781191993b7e52fd7a447f196803 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -458,6 +458,7 @@ EXTEND
     [ id = IDENT -> id, None, []
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
         id, None, vars
+    | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars
     ]
   ];
   binder: [