From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 8 Jul 2014 13:46:10 +0000 (+0000)
Subject: update for CamlP5
X-Git-Tag: make_still_working~876
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc5516f15988620e9b152c6c741daae4a4c4fb0c;p=helm.git

update for CamlP5
---

diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index f17459162..4ee9ad4e6 100644
--- 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 95b688c54..587c22e4a 100644
--- 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 941bb2218..b1362b0f6 100644
--- 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 893a3f53c..47f42356f 100644
--- 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 25e67131f..119f13093 100644
--- 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