update for CamlP5

diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index f17459162ce81c0ad9c5352cca5e9d99f43cb81c..4ee9ad4e61836051d85210afc6a8714a0325400a 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend.opt
+++ b/helm/software/components/binaries/transcript/.depend.opt
@@ -1,24 +1,24 @@
-gallina8Parser.cmi: types.cmx 
-grafiteParser.cmi: types.cmx 
-grafite.cmi: types.cmx 
-engine.cmi: 
-types.cmo: 
-types.cmx: 
-options.cmo: 
-options.cmx: 
-gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi 
-gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
-gallina8Lexer.cmo: options.cmx gallina8Parser.cmi 
-gallina8Lexer.cmx: options.cmx gallina8Parser.cmx 
-grafiteParser.cmo: types.cmx options.cmx grafiteParser.cmi 
-grafiteParser.cmx: types.cmx options.cmx grafiteParser.cmi 
-grafiteLexer.cmo: options.cmx grafiteParser.cmi 
-grafiteLexer.cmx: options.cmx grafiteParser.cmx 
-grafite.cmo: types.cmx options.cmx grafite.cmi 
-grafite.cmx: types.cmx options.cmx grafite.cmi 
+gallina8Parser.cmi: types.cmx
+grafiteParser.cmi: types.cmx
+grafite.cmi: types.cmx
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
+gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
+gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
+gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
+gallina8Lexer.cmx: options.cmx gallina8Parser.cmx
+grafiteParser.cmo: types.cmx options.cmx grafiteParser.cmi
+grafiteParser.cmx: types.cmx options.cmx grafiteParser.cmi
+grafiteLexer.cmo: options.cmx grafiteParser.cmi
+grafiteLexer.cmx: options.cmx grafiteParser.cmx
+grafite.cmo: types.cmx options.cmx grafite.cmi
+grafite.cmx: types.cmx options.cmx grafite.cmi
 engine.cmo: types.cmx options.cmx grafiteParser.cmi grafiteLexer.cmx \
-    grafite.cmi gallina8Parser.cmi gallina8Lexer.cmx engine.cmi 
+    grafite.cmi gallina8Parser.cmi gallina8Lexer.cmx engine.cmi
 engine.cmx: types.cmx options.cmx grafiteParser.cmx grafiteLexer.cmx \
-    grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi 
-top.cmo: options.cmx engine.cmi 
-top.cmx: options.cmx engine.cmx 
+    grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi
+top.cmo: options.cmx engine.cmi
+top.cmx: options.cmx engine.cmx

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 95b688c548b0f4565dcecddff4c777e26477c546..587c22e4a07b8b9a39fea3225069c4a73454e01f 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -211,8 +211,8 @@ let extract_term_production 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),
@@ -819,11 +819,11 @@ let exc_located_wrapper f =
   try
     f ()
   with
-  | Stdpp.Exc_located (floc, Stream.Error msg) ->
+  | Ploc.Exc (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
-  | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+  | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
-  | Stdpp.Exc_located (floc, exn) ->
+  | Ploc.Exc (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 
 let parse_level1_pattern precedence lexbuf =

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 941bb221871192ae6ecaf32f7d9dcc75fd54dbb9..b1362b0f648c97bb131cae47537f4c848718d4be 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -1058,13 +1058,13 @@ let exc_located_wrapper f =
   try
     f ()
   with
-  | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
-  | Stdpp.Exc_located (floc, Stream.Error msg) ->
+  | Ploc.Exc (_, End_of_file) -> raise End_of_file
+  | Ploc.Exc (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
-  | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
+  | Ploc.Exc (floc, HExtlib.Localized(_,exn)) ->
       raise
        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
-  | Stdpp.Exc_located (floc, exn) ->
+  | Ploc.Exc (floc, exn) ->
       raise
        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index 893a3f53c9ef2a72e93f57d7ed9187e7901ad18a..47f42356f4854e8f2f08242a9f8d7ec7fb4f3115 100644 (file)
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/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 "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "{@[<hov2> ";
@@ -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 "{@[<hov2> ";
         let todo = visit_symbol sep todo is_son in

diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index 25e67131fca0487c4390d310d8307722b5058067..119f13093a98003e4d06ea0244ce7aae7f76e6e3 100644 (file)
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,5 +1,5 @@
-utf8Macro.cmi: 
-utf8MacroTable.cmo: 
-utf8MacroTable.cmx: 
-utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
-utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
+utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi