X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=587c22e4a07b8b9a39fea3225069c4a73454e01f;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=95b688c548b0f4565dcecddff4c777e26477c546;hpb=b7e730726f5c5ba9b53b80d3881bcacd38a11a67;p=helm.git 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 =