From 17308cc43b38728bc79b4db57314e54049c6f03b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Mar 2011 16:03:55 +0000 Subject: [PATCH] Ported to - camlp5 version 6.02.2 + patches - ocaml version 3.11.2-4 If you are still using the old version of OCaml + Camlp5, do not update these two files. --- matita/components/content_pres/cicNotationParser.ml | 4 ++-- matita/components/grafite_parser/print_grammar.ml | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 53c60820c..6d18fe837 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -208,8 +208,8 @@ let extract_term_production status pattern = match magic with | Ast.List0 (_, None) -> Gramext.Slist0 s | Ast.List1 (_, None) -> Gramext.Slist1 s - | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l) - | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l) + | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false) + | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false) | _ -> assert false in [ Env (List.map Env.list_declaration p_names), diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml index 5bc87f247..738ceb4da 100644 --- a/matita/components/grafite_parser/print_grammar.ml +++ b/matita/components/grafite_parser/print_grammar.ml @@ -87,7 +87,7 @@ and is_symbol_dummy = function | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt | Snterm e | Snterml (e, _) -> is_entry_dummy e | Slist1 x | Slist0 x -> is_symbol_dummy x - | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y + | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y | Sopt x -> is_symbol_dummy x | Sself | Snext -> false | Stree t -> is_tree_dummy t @@ -186,7 +186,7 @@ let visit_description desc fmt self = let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo - | Slist0sep (symbol,sep) -> + | Slist0sep (symbol,sep,false) -> Format.fprintf fmt "[@[ "; let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; @@ -200,7 +200,7 @@ let visit_description desc fmt self = let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]}+ @ "; todo - | Slist1sep (symbol,sep) -> + | Slist1sep (symbol,sep,false) -> let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; let todo = visit_symbol sep todo is_son in -- 2.39.2