minor correction on "source" production

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 91086b46d71027bd15b550132fb0fad379c2a52f..24cade68afae5be4544d3ade1df050e5cff2bab2 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -500,7 +500,7 @@ EXTEND
   index: [[ b = OPT SYMBOL "-" -> match b with None -> true | _ -> false ]];
 
   source: [[
-     src = OPT IDENT "implied" ->
+     src = OPT [ IDENT "implied" ] ->
         match src with None -> `Provided | _ -> `Implied
   ]];