]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content_pres/cicNotationParser.ml
(no commit message)
[helm.git] / matitaB / components / content_pres / cicNotationParser.ml
index 7522d3c792546a9e042f64aeda9cda048887a21d..6736211d4e67fbf5b88990b1bf93535f74b2d5e9 100644 (file)
@@ -30,6 +30,8 @@ open Printf
 module Ast = NotationPt
 module Env = NotationEnv
 
+let prerr_endline _ = () 
+
 exception Parse_error of string
 exception Level_not_found of int
 
@@ -322,9 +324,9 @@ let extract_term_production status pattern =
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
           | Ast.List0 (_, Some l) -> 
-              Gramext.Slist0sep (s, gram_of_literal status l)
+              Gramext.Slist0sep (s, gram_of_literal status l,true)
           | Ast.List1 (_, Some l) -> 
-              Gramext.Slist1sep (s, gram_of_literal status l)
+              Gramext.Slist1sep (s, gram_of_literal status l,true)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),